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 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).
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
Publications and Documents
[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].
[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.
[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, jointly with a paper by Guiraud, Malbos, and Mimram.
[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.
[C2] Accattoli, Kesner. The Structural Lambda-Calculus. CSL 2010.
[C1] Accattoli, Guerrini. Jumping Boxes. Representing Lambda-Calculus Boxes By Jumps. CSL 2009.
[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].
None at the moment.
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.
Accattoli, Guerrieri, Leberle. Semantic Bounds and Strong Call-by-Value Normalization.
[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.