Enrico Tassi Homepage

Date: 2017-02-17

Foto 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.

I'm developing Coq with the aim of making it scale well to large libraries of formalized mathematics. In particular I'm working on the Paral-ITP project.

Here my detailed curriculm vitae in english.



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.


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


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:


Some software I worked on as part of my job:

Some software I worked on in my spare time: