Beniamino Accattoli

Currently, I am post-doc at Bologna University, supervised by Ugo Dal Lago and Andrea Asperti.

My previous affiliations have been:
- 2012-2013: Post-doc at Carnegie Mellon University (Pittsburgh, USA), working with Frank Pfenning on the meta-CLF project;
- 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).

My interests:
  1. Proof theory: classic, intuitionistic and linear logic and their fragments/variants/extensions/interpretations;
  2. Analysis and Implementation of higher-order programming languages: lambda calculus, explicit substitutions, abstract machines, operational semantics, cost models;
  3. Graphical syntaxes: graph rewriting, proof nets, correctness criteria, boxes, jumps;
  4. Rewriting theory: normalization and confluence, higher-order, non-orthogonal, and abstract rewriting, residual theory, permutation equivalence and standardization, rewriting modulo.
  5. 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.
 
Events:

Papers:

    Journals:

    Conferences:

    Workshops:
 
    Submitted:

Notes:

Formalizations:

Ph.D Thesis:
 
Talks: 
  • 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 2013It 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.