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


My research topic. I study higher-order computations, the approach to computation where the inputs and the outputs of a program are not simply numbers, strings, or compound data types but also programs themselves. I mainly study the lambda calculus, the mathematical core formalism for higher-order computations, using a combination of tools from logic, graphical syntaxes, rewriting theory, computational complexity, denotational semantics, concurrency, and implementations of programming languages.

The main fields of application are functional programming languages such as OCaml or Haskell, but functional features are nowadays also found in mainstream languages such as Java or Python, and proof assistants such as Coq or Agda. In addition, the lambda-calculus is also of interest for its mathematical connections to proof theory and category theory.

Bird's Eye View. My research work is an attempt to connect different tools and perspectives in the study of the lambda calculus. There are two main recurrent and correlated themes in my work, one of an internal nature and one of an external nature:

  • Internal: connecting the classical mathematical theory of the lambda calculus with the practice of the implementations of functional languages, by building a mathematical theory of sharing, the crucial ingredient for efficiency;

  • External: reconciling the schism between the lambda calculus and computational complexity, by studying reasonable cost models for time and space in the lambda calculus.

Both topics have been reshaped by the results that I have obtained in a number of collaborations. In particular, I was involved in the solution of three long-standing open problems:

  1. Sharing: finding the canonical lambda calculus with first-class sharing. The lambda calculus can be enriched with sharing (or explicit substitutions) in many different ways. Since the 1990s many calculi have been proposed, usually with complex theories and unable to preserve the properties of the lambda calculus. In collaboration with Delia Kesner, I introduced the linear substitution calculus, which is simpler than all previously calculi, preserves the properties of the lambda calculus, and has some properties that the lambda calculus does not (for instance, postponement of garbage collection and confluence in the weak case). See papers [C5,C6,C10,C22] below.

  2. Time: finding the first reasonable time cost model for the lambda calculus. In collaboration with Ugo Dal Lago, I proved that the lambda calculus is a reasonable computational model for time, 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). This is my most important contribution, and a major development in the theory of lambda calculus.

  3. Logarithmic space: finding the first reasonable space cost model for the lambda calculus accounting for logarithmic space. Logarithmic space has to be measured via an abstract machine, and it was conjectured that one had to use token-based machines, because environment-based ones could not be space reasonable (that is, equivalent to Turing machines). In collaboration with Ugo Dal Lago and Gabriele Vanoni, we first refuted the conjecture about token-machines in paper [C32] below, and then in [C36] we introduced an environment-based machine that, against expectations, provides the first reasonable cost model for logarithmic space.


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

Recent and Forthcoming Events:

  • MPRI, lecturer. Lecture notes and slides are here.


Projects:

Publications and Documents

Dblp entry and google scholar.


Journal Papers:


Conference Papers:








  • [C14] Accattoli, Sacerdoti Coen. On the Relative Usefulness of Fireballs. LICS 2015. The version linked here corrects a few typos wrt the official one. This paper has been considerably improved and simplified by [C18], in turn improved by [J5].







Invited Papers:


Workshop Papers:

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


Submitted:

  • None at the moment.

Unpublished:


Notes:


Formalizations:


PhD Thesis:

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

Past Events

2022:

2021:

2020:

2019:

2018:

2017: