Enrico Tassi Homepage

Date: 2018-07-18

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

Here my detailed curriculm vitae in english.

Contacs:

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.

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:

Software

Some software I worked on as part of my job:

Some software I worked on in my spare time: