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.

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. A notable byproduct of this line of research is the Hierarchy-Builder tool used in the Mathematical Components library and in the CoREACT ANR project.

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 (retired) proud Debian developer.

Papers

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

Debian

I've been a Debian developer from 2006 to 2016. I like to think of Debian as the best O.S. for developers (and not only for users), so I was involved in pushing the awesome Lua language into Debian.

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 work on as part of my job:

• Elpi extension language.
• Coq proof assitant.
• SSR extension for the Coq 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).