معرفی
Enrico Tassi is a researcher at Inria, France, affiliated with the STAMP team. His work focuses on the technology of formal proofs, particularly type theory, interactive theorem proving, and its application to formalizing mathematics. He is a key contributor to the development of tools like Coq-Elpi, Hierarchy-Builder, and the small scale reflection Coq extension. His research spans proof assistant architecture, software design, and formal verification, with a strong emphasis on free software principles.
Enrico completed his Ph.D. at the University of Bologna in 2008, where he designed the Matita interactive theorem prover. He contributed to the formalization of the Odd Order Theorem and the Paral-ITP project, aiming to scale Coq for large mathematical libraries. His software projects include Elpi, a meta-language for proof assistants, and past contributions to Debian as a developer (2006–2016), focusing on integrating the Lua language into Debian systems.
His publications highlight innovations in unification algorithms, tactical design, and proof structuring techniques. Articles address challenges in bi-directional type inference, pattern-based proof command focusing, and nonuniform coercion implementations. His work on small-scale reflection and Hierarchy-Builder demonstrates expertise in algebraic hierarchies and formal library management. Current efforts target enhancing OCaml-based systems through Elpi's high-level programming capabilities.
- Key Collaborations: Mathematical Components team (INRIA), D.A.M.A. Project
- Major Tools: Coq-Elpi, Hierarchy-Builder, Matita
- Formalization Efforts: Ordered Uniformities, Odd Order Theorem, Finite Group Theory
