Beniamino Accattoli

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

My research concerns higher-order computation, i.e. that approach to computation where the inputs and the output of a program are not simply numbers, strings, or compound datatypes but programs themselves. I use a combination of tools from (linear) logic, graphical syntaxes, rewriting theory, computational complexity, concurrency, formalized reasoning, and implementations of programming languages.

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

Internship Proposal:





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

  • [N1] B. Accattoli. A linear analysis of call-by-value lambda-calculus.  Subsumed by [S1].


PhD Thesis:
  • CSL-LICS 2014.
  • On the Formalization of Lambda-Calculus 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 2013It 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 mini-course 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.
Subpages (1): Lambda to Pi Internship