I am a researcher in computer science at Inria, in the PARTOUT team (the evolution of the PARSIFAL team), since January 2015. My research is about higher-order computation, that approach to computation where the inputs and the outputs of a program are not simply numbers, strings, or compound datatypes 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) is the proof 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). : "givenname"."familyname" at inria.frE-mailEvents 2020:Projects:- COCA HOLA, October 2016-September 2020.
Papers: Journals:- [J6] Accattoli, Graham-Lengrand, Kesner. Tight Typings and Split Bounds, Fully Developed. Accepted for publication in the
*Journal of Functional Programming*. - [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].
- [C28] Accattoli, Díaz-Caro. Functional Pearl: the Distributive Lambda Calculus.
*FLOPS 2020*.
- [C27] Accattoli, Faggian, Guerrieri. Factorization and Normalization, Essentially.
*APLAS 2019*. *[C26]*Accattoli, Sacerdoti Coen. Sharing Equality is Linear.*Condoluci,**PPDP**2019*.Accattoli, Condoluci, Guerrieri, Sacerdoti Coen. Crumbling Abstract Machines.*[C25]**PPDP**2019*.- [C24] Accattoli, Guerrieri, Leberle. Types by Need.
*ESOP 2019*.
Accattoli, Guerrieri. Types of Fireballs.*[C23]**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*. One of the reviewers wrote this paragraph. Enjoy :) - [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. Improved by [C18] above.
- [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*. Version with proofs (in the appendix).
- [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*. - [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:Accattoli. A Fresh Look at the lambda Calculus.*[I3]**Invited paper at FSCD 2019*Slides of the invited talk.*.*Accattoli. (In)Efficiency and Reasonable Cost Models.*[I2]*It builds on the two notes*Invited paper at LSFA 2017.**[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.*
Workshops:*[W2] Accattoli. Evaluating functions as processes. TERMGRAPH 2013.*
J2*[W1] Accattoli. Proof nets and the call-by-value lambda calculus. LSFA 2012. Subsumed by [**].*
Submitted:- [S1] Accattoli, Dal Lago, Vanoni. The Abstract Machinery of Interaction.
Unpublished:- [U1] Accattoli, Faggian, Guerrieri. Factorize Factorization.
Notes:- [N3] Accattoli. The Maximal MAM, a Reasonable Implementation of the Maximal Strategy. Unpublished but used in
.*[I2]* *[N2] Dal Lago, Accattoli. Encoding Turing Machines Into the Deterministic Lambda-Calculus. It is a more detailed reformulation of a technical result in*Unpublished but used in*[C5].*.*[I2]**[N1] Accattoli. A linear analysis of call-by-value lambda-calculus.**Subsumed by [**J2].*
Formalizations:PhD Thesis:
Old Events: |