CV

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.