معرفی
Enrico Tassi is a researcher at INRIA (French Institute for Research in Computer Science and Automation) in the STAMP research team. He obtained his Ph.D. from the University of Bologna in 2008, where he worked on the design and implementation of the Matita interactive theorem prover. His research primarily focuses on the technology of formal proofs, particularly type theory implementation and mathematical modeling.
Education:
- Ph.D. in Computer Science, University of Bologna (2008)
Tassi's research explores interactive theorem provers, functional programming, and logic programming. He maintains the small scale reflection extension for Coq and develops the Elpi extension language to enhance OCaml software capabilities. His work enables advanced manipulation of mathematical structures and formal proof environments through high-level programming constructs.
His publications demonstrate consistent focus on theorem proving, formal methods, and programming language theory. Recent works emphasize practical implementations in proof assistants (Matita, Coq), unification algorithms, and formal verification of mathematical theories including measure theory and algebra.
Tassi has contributed to significant projects including the Mathematical Components library (formalizing the Odd Order Theorem), the Paral-ITP project (scaling Coq for large mathematical libraries), and the CoREACT ANR project. He develops open-source tools including Coq-Elpi plugin and Hierarchy-Builder.
He serves on program committees for conferences including CPP, CoqPL and FLOPS. While retired from Debian development (2006-2016), he maintains involvement in open-source communities.
