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


My research: I study higher-order computations, that approach to computation where the inputs and the outputs of a program are not simply numbers, strings, or compound data types 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, I proved 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).


Research lines: my research work can be seen as an effort to inter-connect different topics in the study of higher-order computations, ranging from denotational semantics to implementations, passing through rewriting theory, complexity analysis, and graphical formalisms. My papers can be classified as belonging to the following entangled research lines.

  • Term and proof representations.

  • Simplified theory of explicit substitutions.

  • Rewriting theory of the lambda calculus and linear logic.

  • Reasonable cost models for the lambda calculus.

  • Complexity analysis and logical foundation of implementation techniques (abstract machines and sharing).

  • Development of a solid theory of call-by-value.

  • Development of a solid theory of call-by-need.

  • Operational bounds from denotational semantics via intersection types.

  • Computational content of game semantics and the geometry of interaction.

  • Formalization of the theory of the lambda calculus.


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

Events 2020-21:


Projects:

Journal Papers:


Conference Papers:













Invited Papers:


Workshop Papers:

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


Submitted:

Unpublished:


Notes:


Formalizations:


PhD Thesis:

  • Jumping around the box: graphical and operational studies on Lambda Calculus and Linear Logic.

Old Events

2020:

2019:

2018:

2017: