Beniamino Accattoli

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

My research is about higher-order computation, i.e. 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 use a combination of tools from (linear) logic, graphical syntaxes, rewriting theory, computational complexity, concurrency, formalised 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 [J2].

  • [S1] B. Accattoli, C. Sacerdoti Coen. On the Value of Variables. Long version of [C12], submitted to Information & Computation (special issue of WoLLIC 2014).
  • [S2] B. Accattoli, G. Guerrieri. Open Call-by-Value. Preprint. It was submitted and rejected, essentially because our comparative study does not cover the sequent calculus approach. I keep the draft online because it is a nice paper, carefully crafted, and easy to read.

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


PhD Thesis: