Beniamino Accattoli

I am a researcher in computer science at Inriain the PARTOUT team (the evolution of the PARSIFAL team), since January 2015.

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).

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

Events 2020:





    Invited papers:

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




PhD Thesis:
Old Events: