I am a researcher in computer science at INRIA, in the PARSIFAL team.
My research is about higher-order computation, i.e. 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).
My previous affiliations have been:
- 2013-2014: Post-doc at Bologna University, supervised by Ugo Dal Lago;
- 2012-2013: Post-doc at Carnegie Mellon University, supervised by Frank Pfenning
- 2010-2011: ATER at Paris 13 University in the LIPN lab (Villetaneuse, France);
- 2009-2010: ATER at Paris 7 University in the PPS lab (Paris, France), during the fourth year of my PhD.
E-mail: "givenname"."familyname" at inria.fr
- [W1] B. Accattoli. Proof nets and the call-by-value lambda calculus. LSFA 2012. Subsumed by [J2].
- [S1] B. Accattoli, C. Sacerdoti Coen. On the Value of Variables. Long version of [C12], submitted to Information & Computation (special issue of WoLLIC 2014).
- [S2] B. Accattoli, G. Guerrieri. Open Call-by-Value. Preprint. It was submitted and rejected, essentially because our comparative study does not cover the sequent calculus approach. I keep the draft online because it is a nice paper, carefully crafted, and easy to read.
- [N1] B. Accattoli. A linear analysis of call-by-value lambda-calculus. Subsumed by [J2].
- LICS 2015.
- Lambda-calculus, Sharing, and Time Cost Models, invited talk at the International Workshop on Logic and Computational Complexity 2015.
- CSL-LICS 2014.
- On the Formalization of Lambda-Calculus Confluence and Residuals, invited talk at the International Workshop on Confluence 2014.
- POPL 2014.
- A Fresh Look at Linear Head Reduction, talk given at the University of Bath, the 20th November 2013, and at Roma Tre University, the 20th December 2013.
- Toward a New Theory of Exponential Proof Nets, talk given at the Chocola meeting at the ENS Lyon, the 14th November 2013, essentially merging together the talks given at LICS and RTA 2013, with a few additional details.
- LICS 2013.
- RTA 2013.
- TERMGRAPH 2013. It has also been presented as a seminar for the Parsifal INRIA team at the LIX lab of the Ecole Polytechnique in May 2013.
- CPP 2012.
- RTA 2012. This is about the work on cost models in collaboration with Ugo Dal Lago. It has also been presented at WST 2012 and DICE 2012, at Carnegie Mellon University and McGill University (both in April 2012), Ecole Polytechnique (July 2012), and University of Minnesota (February 2013).
- In March and October 2012 I taught a mini-course about my research work at the University of Brasilia and at the University of Buenos Aires, respectively. The description and the slides of the more recent version are here.