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 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
Dblp entry and google scholar.
Journal Papers:
[J7] Accattoli. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. Logical Methods in Computer Science 2023, 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. Logical Methods in Computer Science 2016, special issue of CSL-LICS 2014. Long version of [C11].
[J2] Accattoli. Proof nets and the call-by-value lambda calculus. Theoretical Computer Science 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. Logical Methods in Computer Science 2012. Subsumes and considerably strengthens the results about termination in [C2].
Conference Papers:
[C45] Accattoli, Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. FSCD 2024. This is the submitted version, the final one will be ready soon.
[C44] Accattoli, Lancelot. Mirroring Call-by-Need, or Values Acting Silly. FSCD 2024. This is the submitted version, the final one will be ready soon.
[C43] Accattoli, Lancelot. Light Genericity. FoSSaCS 2024.
[C42] Accattoli. Semantic Bounds from Multi Types, Revisited. CSL 2024.
[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. Subsumed by [J7].
[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.
[C4] Accattoli, Paolini. Call-by-value solvability, revisited. FLOPS 2012. Version with proofs appendix.
[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.
[I3] Accattoli. A Fresh Look at the lambda Calculus. Invited paper at FSCD 2019. Slides of the invited talk.
[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.
Workshop Papers:
[W2] Accattoli. Evaluating functions as processes. TERMGRAPH 2013. Ten years later, this work has been refined, extended, and formalized in [C39].
[W1] Accattoli. Proof nets and the call-by-value lambda calculus. LSFA 2012. Subsumed by [J2].
Submitted:
[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.
Unpublished:
[U3] Accattoli, Faggian, Lancelot. Normal Form Bisimulations by Value, 2022.
[U2] Accattoli, Guerrieri. Call-by-Value Solvability and Multi Types, 2022. 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, 2021. The part about semantic bounds is better developed and published in [C42] (but in call-by-name rather than in call-by-value) and the part about strong call-by-value normalization is reformulated in [C41] by comparing it with another notion of normalization and removing the technical aspect of exact bounds.
Notes:
[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].
PhD Thesis:
Jumping around the box: graphical and operational studies on Lambda Calculus and Linear Logic.
Past Events
2023:
PPDP 2023, PC.
ESSLLI 2023, course lecturer (the course material is here) and invited evening lecturer.
2022:
PPDP 2022, PC co-chair.
LSFA 2022, PC member.
APLAS 2022, PC member.
MPRI, lecturer.
2021:
2020:
LSFA 2020, PC member.
IWC 2020, PC member.
TERMGRAPH 2020, PC member.
MPRI, lecturer.
2019:
2018:
2017: