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 various collaborations. In particular, I was involved in the solution of three long-standing open problems:
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.
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.
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
Publications and Documents
[J7] Accattoli. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. Accepted for the LMCS special issue of LICS 2022. Long version of [C35].
[J6] Accattoli, Graham-Lengrand, Kesner. Tight Typings and Split Bounds, Fully Developed. Journal of Functional Programming 2020, special issue of ICFP 2018. Long version of [C21].
[J5] Accattoli, Guerrieri. Abstract Machines for Open Call-by-Value. Science of Computer Programming 2019, special issue of FSEN 2017. Long version of [C18].
[J4] Accattoli, Sacerdoti Coen. On the Value of Variables. Information & Computation 2017, special issue of WoLLIC 2014. Long version of [C12].
[J3] Accattoli, Dal Lago. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. LMCS 2016, special issue of CSL-LICS 2014. Long version of [C11].
[J2] Accattoli. Proof nets and the call-by-value lambda calculus. TCS 2015, special issue of LSFA 2012. Long version of [W1], subsuming also [N1].
[J1] Accattoli, Kesner. Preservation of strong normalisation modulo permutation for the structural lambda-calculus. LMCS 2012. Subsumes and considerably strengthens the results about termination in [C2].
[C42] Accattoli. Semantic Bounds from Multi Types, Revisited. Accepted at CSL 2024. The version linked here is the submitted one, the final version will be ready soon.
[C41] Accattoli, Guerrieri, Leberle. Strong Call-by-Value and Multi Types. ICTAC 2023.
[C40] Accattoli, Barenbaum. A Diamond Machine for Strong Evaluation. APLAS 2023.
[C39] Accattoli, Blanc, Sacerdoti Coen. Formalizing Functions as Processes. ITP 2023.
[C38] Accattoli, Guerrieri. The Theory of Call-by-Value Solvability. ICFP 2022.
[C37] Accattoli, Dal Lago, Vanoni. Multi Types and Reasonable Space. ICFP 2022. Distinguished paper award.
[C36] Accattoli, Dal Lago, Vanoni. Reasonable Space for the lambda-Calculus, Logarithmically. LICS 2022.
[C35] Accattoli. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. LICS 2022.
[C34] Accattoli, Leberle. Useful Open Call-by-Need. CSL 2022. At the end of this paper, a forthcoming companion paper about an abstract machine is mentioned. It will never be completed because in the meantime Biernacka et al. developed here a machine going beyond what we were doing.
[C33] Accattoli, Condoluci, Sacerdoti Coen. Strong Call-by-Value is Reasonable, Implosively. LICS 2021.
[C32] Accattoli, Dal Lago, Vanoni. The Space of Interaction. LICS 2021.
[C31] Accattoli, Dal Lago, Vanoni. The (In)Efficiency of Interaction. POPL 2021.
[C30] Accattoli, Faggian, Guerrieri. Factorize Factorization. CSL 2021.
[C29] Accattoli, Dal Lago, Vanoni. The Machinery of Interaction. PPDP 2020.
[C28] Accattoli, Díaz-Caro. Functional Pearl: the Distributive Lambda Calculus. FLOPS 2020.
[C27] Accattoli, Faggian, Guerrieri. Factorization and Normalization, Essentially. APLAS 2019.
[C26] Condoluci, Accattoli, Sacerdoti Coen. Sharing Equality is Linear. PPDP 2019.
[C25] Accattoli, Condoluci, Guerrieri, Sacerdoti Coen. Crumbling Abstract Machines. PPDP 2019.
[C24] Accattoli, Guerrieri, Leberle. Types by Need. ESOP 2019.
[C23] Accattoli, Guerrieri. Types of Fireballs. APLAS 2018.
[C22] Accattoli. Proof Nets and the Linear Substitution Calculus. ICTAC 2018.
[C21] Accattoli, Graham-Lengrand, Kesner. Tight Typings and Split Bounds. ICFP 2018. Subsumed by [J6] above.
[C20] Accattoli, Barras. The Negligible and Yet Subtle Cost of Pattern Matching. APLAS 2017.
[C19] Accattoli, Barras. Environments and the Complexity of Abstract Machines. PPDP 2017.
[C18] Accattoli, Guerrieri. Implementing Open Call-by-Value. FSEN 2017. Subsumed by [J5].
[C17] Accattoli, Guerrieri. Open Call-by-Value. APLAS 2016.
[C16] Accattoli. The Useful MAM, a Reasonable Implementation of the Strong Lambda-Calculus. WoLLIC 2016. The version linked here has 10 additional pages of appendix, containing proofs omitted from the official version.
[C15] Accattoli, Barenbaum, Mazza. A Strong Distillery. APLAS 2015.
[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].
[C13] Accattoli, Barenbaum, Mazza. Distilling Abstract Machines. ICFP 2014.
[C12] Accattoli, Sacerdoti Coen. On the Value of Variables. WoLLIC 2014. Subsumed by [J4].
[C11] Accattoli, Dal Lago. Beta Reduction is Invariant, Indeed. CSL-LICS 2014. Subsumed by [J3].
[C10] Accattoli, Bonelli, Kesner, Lombardi. A Nonstandard Standardization Theorem. POPL 2014.
[C9] Accattoli. Linear Logic and Strong Normalization. RTA 2013. Best paper award.
[C8] Accattoli. Compressing Polarized Boxes. LICS 2013.
[C7] Accattoli. Proof pearl: Abella formalization of lambda-calculus cube property. CPP 2012.
[C6] Accattoli. An abstract factorization theorem for explicit substitutions. RTA 2012.
[C5] Accattoli, Dal Lago. On the invariance of the unitary cost model for head reduction. RTA 2012.
[C3] Accattoli, Kesner. The Permutative lambda Calculus. LPAR 2012.
[C2] Accattoli, Kesner. The Structural lambda-Calculus. CSL 2010.
[C1] Accattoli, Guerrini. Jumping Boxes. Representing lambda-Calculus Boxes By Jumps. CSL 2009.
Invited Papers and Dissemination Material:
[I4] Accattoli. Sharing a Perspective on the lambda Calculus. Onward! Essays 2023.
[I2] Accattoli. (In)Efficiency and Reasonable Cost Models. Invited paper at LSFA 2017. It builds on the two notes [N2] and [N3].
[I1] Accattoli. The Complexity of Abstract Machines. Invited paper at WPTE 2016. The study of the KAM in section 9 is now superseded and improved by paper [C19] above.
[W2] Accattoli. Evaluating functions as processes. TERMGRAPH 2013.
[W1] Accattoli. Proof nets and the call-by-value lambda calculus. LSFA 2012. Subsumed by [J2].
[S2] Accattoli, Dal Lago, Vanoni. Reasonable Space for the lambda-Calculus, Logarithmically. Extended version of [C36], submitted to the LMCS special issue of LICS 2022.
[U3] Accattoli, Faggian, Lancelot. Normal Form Bisimulations by Value.
[U2] Accattoli, Guerrieri. Call-by-Value Solvability and Multi Types. Please rather refer to [C38], which refines the results in this document and also complements them with many other small results, observations, and discussions.
[U1] Accattoli, Guerrieri, Leberle. Semantic Bounds and Strong Call-by-Value Normalization.
[N4] Accattoli, Dal Lago, Vanoni. A Log-Sensitive Encoding of Turing Machines in the λ-Calculus. Used in [S2].
[N3] Accattoli. The Maximal MAM, a Reasonable Implementation of the Maximal Strategy. 2017. Unpublished but used in [I2].
[N2] Dal Lago, Accattoli. Encoding Turing Machines Into the Deterministic Lambda-Calculus. 2017. It is a more detailed reformulation of a technical result in [C5]. Unpublished but used in [I2].
[N1] Accattoli. A linear analysis of call-by-value lambda-calculus. Subsumed by [J2].
Jumping around the box: graphical and operational studies on Lambda Calculus and Linear Logic.