Beniamino Accattoli

I am a researcher in computer science at INRIAin the PARSIFAL team.

My research is about higher-order 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 lambda-calculus, 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 lambda-calculus is a reasonable computational model, i.e. that it is polynomially related to Turing machines, see paper [j3] below. Our proof solved a long-standing open problem, and in an unexpected way. The lambda-calculus was indeed suspected to be unreasonable because of a negative result due to Asperti and Mairson (in POPL '98).

I started at INRIA in 2015. My previous affiliations have been:
- 2013-2014: Post-doc at Bologna University, supervised by Ugo Dal Lago;
- 2012-2013: Post-doc at Carnegie Mellon University, supervised by Frank Pfenning;
- 2011-2012: Post-doc at INRIA in the PARSIFAL team, supervised by Dale Miller;
- 2010-2011: ATER at Paris 13 University in the LIPN lab (Villetaneuse, France);
2009-2010: ATER at Paris 7 University in the PPS lab (Paris, France), during the fourth year of my PhD.
- 2006-2010: Ph.D. in Computer Engineering at La Sapienza University under the supervision of Stefano Guerrini

E-mail: "givenname"."familyname" at






  • [C25] B. Accattoli, G. Guerrieri, M. Leberle. Types by Need. Accepted to ESOP 2019. This is the submitted version.

  • [W1] B. Accattoli. Proof nets and the call-by-value lambda calculus. LSFA 2012. Subsumed by [J2].




PhD Thesis: