I am a researcher in computer science at INRIA, in the PARSIFAL team.
My research is about higherorder computation, that approach to computation where the inputs and the outputs of a program are not simply numbers, strings, or compound datatypes but programs themselves. I mainly study the lambdacalculus, using a combination of tools from (linear) logic, graphical syntaxes, rewriting theory, computational complexity, concurrency, formalised reasoning, and implementations of programming languages.
My main achievement (in collaboration with Ugo Dal Lago) is the proof that the lambdacalculus is a reasonable computational model, i.e. that it is polynomially related to Turing machines, see paper [j3] below. Our proof solved a longstanding open problem, and in an unexpected way. The lambdacalculus was indeed suspected to be unreasonable because of a negative result due to Asperti and Mairson (in POPL '98).
My previous affiliations have been:  20132014: P ostdoc at Bologna University, supervised by Ugo Dal Lago; 20122013: Postdoc at Carnegie Mellon University, supervised by Frank Pfenning;
 20102011: ATER at Paris 13 University in the LIPN lab (Villetaneuse, France); 20092010: ATER at Paris 7 University in the PPS lab (Paris, France), during the fourth year of my PhD.
Email: "givenname"."familyname" at inria.fr
Events:
Projects: Papers:
Journals:
Conferences:
Workshops:  [W1] B. Accattoli. Proof nets and the callbyvalue lambda calculus. LSFA 2012. Subsumed by [J2].
Submitted:
Notes:  [N1] B. Accattoli. A linear analysis of callbyvalue lambdacalculus. Subsumed by [J2].
Formalizations:
PhD Thesis:
Talks:
 Open CallbyValue, talk given at APLAS 2016.
 The Complexity of Abstract Machines, invited talk at WPTE 2016.
 LICS 2015.
 Lambdacalculus, Sharing, and Time Cost Models, invited talk at the International Workshop on Logic and Computational Complexity 2015.
 CSLLICS 2014.
 On the Formalization of LambdaCalculus Confluence and Residuals, invited talk at the International Workshop on Confluence 2014.
 POPL 2014.
 A Fresh Look at Linear Head Reduction, talk given at the University of Bath, the 20th November 2013, and at Roma Tre University, the 20th December 2013.
 Toward a New Theory of Exponential Proof Nets, talk given at the Chocola meeting at the ENS Lyon, the 14th November 2013, essentially merging together the talks given at LICS and RTA 2013, with a few additional details.
 LICS 2013.
 RTA 2013.
 TERMGRAPH 2013. It has also been presented as a seminar for the Parsifal INRIA team at the LIX lab of the Ecole Polytechnique in May 2013.
 CPP 2012.
 RTA 2012. This is about the work on cost models in collaboration with Ugo Dal Lago. It has also been presented at WST 2012 and DICE 2012, at Carnegie Mellon University and McGill University (both in April 2012), Ecole Polytechnique (July 2012), and University of Minnesota (February 2013).
 In March and October 2012 I taught a minicourse about my research work at the University of Brasilia and at the University of Buenos Aires, respectively. The description and the slides of the more recent version are here.

