Skip to Main content
Number of documents



I'm a researcher at Inria in the Marelle team.
I'm interested in the technology of formal proofs, in particular in
type theory, its implementation and its use to model mathematics.

I defended my Ph.D. at the university of Bologna in 2008, where
I worked on the design and implementation of the
Matita interactive theorem prover.
Then I worked for the Mathematical Components team on the
formalization of the Odd Order theorem.  I'm currently maintaining the
small scale reflection Coq extension used in that project.
In the past I've also worked on on the Paral-ITP project with the
aim of making Coq scale well to large libraries of formalized mathematics, like
the Mathematical Components one.

I'm currently designing and implementing the Elpi extension language to
make it possible to improve the capabilities of software written in OCaml by
using a high level programming language. In particular Elpi gives first class
support for binders and unification variables to ease the implementation of
intricate algorithms as the one performing type inference.  The
Coq-elpi plugin embeds Elpi in Coq and makes it easy to
manipulate Coq terms in Elpi for the purpose of implementing new
commands or tactics.

Journal articles2 documents

  • Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2019, 29 (8), pp.1125-1150. ⟨hal-01410567v3⟩
  • Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink. Coqoon. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017. ⟨hal-01410450⟩

Conference papers15 documents

  • Karl Palmskog, Enrico Tassi, Théo Zimmermann. Reliably Reproducing Machine-Checked Proofs with the Coq Platform. RRRR 2022 - Workshop on Reproducibility and Replication of Research Results, Apr 2022, Munich, Germany. ⟨hal-03592675v2⟩
  • Reynald Affeldt, Xavier Allamigeon, yves Bertot, Quentin Canu, Cyril Cohen, et al.. Porting the Mathematical Components library to Hierarchy Builder. the COQ Workshop 2021, Jul 2021, virtuel- Rome, Italy. ⟨hal-03463762⟩
  • Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi. FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.34:1--34:21, ⟨10.4230/LIPIcs.FSCD.2020.34⟩. ⟨hal-02478907v5⟩
  • Marco Maggesi, Enrico Tassi. Private types in Higher Order Logic Programming. TEASE-LP 2020 - Workshop on Trends, Extensions, Applications and Semantics of Logic Programming, May 2020, Virtual Event, France. ⟨hal-03117762⟩
  • Enrico Tassi. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. ⟨10.4230/LIPIcs.CVIT.2016.23⟩. ⟨hal-01897468v2⟩
  • Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink. Coqoon An IDE for interactive proof development in Coq. TACAS, Apr 2016, Eindhoven, Netherlands. ⟨hal-01242295⟩
  • Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi. Implementing HOL in an Higher Order Logic Programming Language. Logical Frameworks and Meta Languages: Theory and Practice, Jun 2016, Porto, Portugal. pp.10, ⟨10.1145/2966268.2966272⟩. ⟨hal-01394686⟩
  • Benjamin Grégoire, Enrico Tassi. Boolean reflection via type classes. Coq Workshop, Aug 2016, Nancy, France. ⟨hal-01410530⟩
  • Bruno Barras, Carst Tankink, Enrico Tassi. Asynchronous processing of Coq documents: from the kernel up to the user interface. Proceedings of ITP, Aug 2015, Nanjing, China. ⟨hal-01135919⟩
  • Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. ELPI: fast, Embeddable, λProlog Interpreter. Proceedings of LPAR, Nov 2015, Suva, Fiji. ⟨hal-01176856⟩
  • Frédéric Chyzak, Assia Mahboubi, Thomas Sibut-Pinote, Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3). ITP - 5th International Conference on Interactive Theorem Proving, 2014, Vienna, Austria. ⟨hal-00984057⟩
  • Georges Gonthier, Andrea Asperti, Jeremy Avigad, yves Bertot, Cyril Cohen, et al.. A Machine-Checked Proof of the Odd Order Theorem. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩. ⟨hal-00816699⟩
  • Assia Mahboubi, Enrico Tassi. Canonical Structures for the working Coq user. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.19-34, ⟨10.1007/978-3-642-39634-2_5⟩. ⟨hal-00816703v2⟩
  • Bruno Barras, Lourdes del Carmen Gonzalez Huesca, Hugo Herbelin, yann Régis-Gianas, Enrico Tassi, et al.. Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. MKM/Calculemus/DML, Jul 2013, Bath, United Kingdom. pp.359-363. ⟨hal-00908980⟩
  • Georges Gonthier, Enrico Tassi. A language of patterns for subterm selection. ITP, Aug 2012, Princeton, United States. pp.361-376, ⟨10.1007/978-3-642-32347-8_25⟩. ⟨hal-00652286v2⟩

Preprints, Working Papers, ...1 document

  • Enrico Tassi. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). 2018. ⟨hal-01637063⟩

Reports3 documents

  • Georges Gonthier, Assia Mahboubi, Enrico Tassi. A Small Scale Reflection Extension for the Coq system. [Research Report] RR-6455, Inria Saclay Ile de France. 2016. ⟨inria-00258384v17⟩
  • Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, et al.. Coq 8.4 Reference Manual. [Research Report] Inria. 2014. ⟨hal-01114602⟩
  • Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory. [Research Report] RR-6156, INRIA. 2007, pp.17. ⟨inria-00139131v2⟩