My previous affiliations have been:
- 2011-2012: Post-doc at INRIA & École Polytechnique (Palaiseau, France) in the PARSIFAL INRIA team, supervised by Dale Miller;
- 2010-2011: ATER at Paris 13 University in the LIPN lab (Villetaneuse, France);
- 2006-2010: Ph.D. in Computer Engineering at La Sapienza University (Rome, Italy) under the supervision of Stefano Guerrini. During the fourth year (2009-2010) of my Ph.D. I have also been ATER at Paris 7 University in the PPS lab (Paris, France).
- Proof theory: classic, intuitionistic and linear logic and their fragments/variants/extensions/interpretations;
- Analysis and Implementation of higher-order programming languages: lambda calculus, explicit substitutions, abstract machines, operational semantics, cost models;
- Graphical syntaxes: graph rewriting, proof nets, correctness criteria, boxes, jumps;
- Rewriting theory: normalization and confluence, higher-order, non-orthogonal, and abstract rewriting, residual theory, permutation equivalence and standardization, rewriting modulo.
- Proof assistants and proof-search: formalization of the theory of lambda-calculus, higher-order abstract syntax and nominal approaches, logical frameworks, unification, implementations of linear forward-chaining.
- B. Accattoli, U. Dal Lago. Beta Reduction is Invariant, Indeed. Accepted to LICS/CSL 2014. This is the submitted version.
- B. Accattoli, E. Bonelli, D. Kesner, C. Lombardi. A Nonstandard Standardization Theorem. POPL 2014.
- B. Accattoli. Linear Logic and Strong Normalization. RTA 2013. Best paper award, jointly with a paper by Guiraud, Malbos, and Mimram. BibTeX.
- B. Accattoli. Compressing Polarized Boxes. LICS 2013. Version with proofs (in the appendix). BibTeX.
- B. Accattoli. Proof pearl: Abella formalization of lambda-calculus cube property. CPP 2012. BibTeX.
- B. Accattoli. An abstract factorization theorem for explicit substitutions. RTA 2012. BibTeX.
- B. Accattoli, U. Dal Lago. On the invariance of the unitary cost model for head reduction. RTA 2012. BibTeX.
- B. Accattoli, L. Paolini. Call-by-value solvability, revisited. FLOPS 2012. BibTeX.
- B. Accattoli, D. Kesner. The Permutative Lambda-Calculus. LPAR 2012. BibTeX.
- B. Accattoli, D. Kesner. The Structural Lambda-Calculus. CSL 2010. BibTeX.
- B. Accattoli, S. Guerrini. Jumping Boxes. Representing Lambda-Calculus Boxes By Jumps. CSL 2009. BibTeX.
- 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.