Enrico Tassi Homepage

I'm a researcher at Inria in the Stamp team.

I'm interested in the technology of formal proofs, in particular in type theory, its implementation and its use to model mathematics and produce bug-free software.

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 Rocq-elpi plugin embeds Elpi in Rocq and makes it easy to manipulate Rocq terms in Elpi for the purpose of implementing new commands or tactics.

I recently defended my HDR: "Elpi: rule-based extension language".

Over the years I contributed to various projects: the mechanization of the Odd Order theorem; the Mathematical Components library; the Small Scale Reflection proof language; the Hierarchy Builder library structuring tool; the Paral-ITP ANR project; the CoREACT ANR project; the Matita interactive theorem prover.

Here my detailed curriculm vitae in english.

Contacs:

• Mail: name.lastname@inria.fr
• Phone: +33 4 92 38 78 19
• Office address: Inria Sophia Antipolis, 2004 route des Lucioles – BP 93, 06902 Sophia Antipolis Cedex, France

Interests

My main research interest is the technology of formal proofs. In particular type theory, its implementation and its use to formalize mathematics.

I'm also interested in all the aspects of software writing, from its design to its implementation. Here you can find some of the softwares I develop in my spare time.

Finally I'm a Free Software supporter and a proud Debian developer.

Papers

Starting from 2013, all my publications are available via HAL. Older publications are available in a separate page.

Students & co

I (co)advised/supervised these PhD students, post-doc, interns and engineers:

• Davide Fissore: “Elaboration in Type Theory via Logic Programming”. Davide continues the work from his master's thesis by designing and implementing a new, improved elaborator for the Rocq system. He is specifi cally focusing on enhancing the resolution of type classes.
• Marco Ferrara: “A mechanization of G”. Marco is working on a mechanization in Rocq of the G logic, the foundation of the Abella prover.
• Matteo Calosci: “A semantics for Hierarchy Builder”. Matteo formalized the semantics of the HB language and reworked some lower layers of the Mathematical Components library.
• Paolo Torrini: “Hierarchy Builder for double categories”. Paolo added to the Hierarchy-Builder tool the capability of mixing interfaces on related, but different, subjects.
• Hjalte Dalland, Jakob Israelsen and Simon Kristensen: “Expanding Coq with Type Aware Code Completion”. Hjalte, Jakob and Simon developed theorem-name completion algorithms to be used in the VSRocq user interface.
• Romain Tetley: “VSRoq”. Romain was involved in the complete rewrite of the VSCoq extension for VSCode together with Maxime Dénès. This effort is meant to continue for a few years and provide a modern and stable user interface for Rocq.
• Thomas Portet: “Hierarchy Builder Instance Saturation”. In the context of LIBERABACI, Thomas improved the ergonomic of Hierarchy Builder by making the order in which certain commands are given irrelevant.
• Julien Wintz: “ADT Elpi”. Julien implemented an execution-trace browser for Elpi programs in the VSCode editor as part of an ADT executed in 2022.
• Luc Chabassier: “Program synthesis from Coq data type declarations”. Luc used an early prototype of Rocq-Elpi to synthesize automatically programs out of data type declarations. In particular he worked on the systesys of equality tests and their correctness proof.
• Matej Kosic: “Coq API and benchmarks”. Matej worked improved the Coq APIs used by Coq plugins and developed a benchmark system for Coq.
• Cvetan Dunchev: “Indexing Elpi rules via term hashes”. Cvetan worked on the implementation of Elpi and in particular he designed a more efficient term representation and an indexing data structure based on term-hashes.
• Karst Tankink: ParalITP ANR project. Karst developed a PIDE backedn for Coq, making it possible to use Coq in conjunction with the Jedit editor and the Eclipse IDE via the dedicated Coqoon plugin.
• François Poulain: DoCoq DIGITEO project. François worked on interfacing the Coq system with the TeXmacs document editor in order to experiment with the rendering and edition of bi-dimensional mathematical notations (e.g. fractions, iterated sums or integrals).

Debian

Since January 2006 I'm a Debian developer. You can have a look at the full list of packages I maintain. I like to think of Debian as the best O.S. for developers (and not only for users), so I'm involved in pushing the awesome Lua language into Debian, with special effort in making developers life easier.

These are my public GPG keys:

• 0x0123F2F2 (fingerprint: 60D0 4388 E385 3643 807B 9507 EE49 1C3E 0123 F2F2, old 1K DSA)
• 0xA29B764F (fingerprint: C11A 5053 569A 7C8C 1758 E311 2505 33CC A29B 764F, new 4K RSA)

Software

Some software I worked on as part of my job:

• Elpi extension language and its Rocq-elpi integration in Rocq.
• Rocq proof assitant and VSRocq VSCode extension.
• Mathamatical Components library for the Rocq system.
• Hierarchy Builder extension for the Rocq system.
• Small Scale Reflection extension for the Rocq system.
• Matita proof assistant.

Some software I worked on in my spare time:

• Sync Mail Dir a Maildir synchronization tool set.
• Libreria, to register all your books (Italian only).
• FreePOPs, an extensible POP3 server that superseded LiberoPOPs (lost interest).
• G3CP is an online theorem prover based on Gentzen's sequent calculi (dead).
• User Level Networking is a Linux kernel patch providing a fine grained access control to network devices (dead).
• Icebreaker, an addictive click&run game, similar to the old Jezzball (development dead).
• Biblioteca, to register all your books (Italian only, dead).
• Fantacalcio, prepare your team and send it by mail (dead, Italian only).
• SaveMyModem An anti-spam/mail-shaper/delete-on-server software (dead).
• ebiff An extensible mail notification agent (dead).