In a proof assistant like Coq, a single mathematical object can often be formalised with several data structures. For instance, integers can be represented in a unary encoding, a binary encoding, etc. Although this is a frequent situation in a programming context, this level of expressivity obstructs proof automation. The global topic of my PhD is using meta-programming to create preprocessing tools targeting statements to be proved in Coq, harnessing relations between types.
During my first year, I released a prototype of preprocessing plugin for Coq, Trakt. Here, the notion of relation between types is an embedding from a source type to a target type. The tool traverses the Coq goal in a recursive way, and makes a new goal along with a proof allowing to replace the old one with the new one in a certified way. Trakt has been integrated successfully to SMTCoq, a proof automation plugin connecting Coq to SMT solvers. Since then, I focus my efforts on Trocq, a second prototype based on parametricity, where the relations between types lie in a hierarchy of structures, going from structure-less relations to full-blown type equivalence.
I write my Coq plugins in the Coq-Elpi language, an implementation of λProlog with easy access to the Coq API and nice features to handle Coq terms.
- Meta-Programming for Proof Transfer in Dependent Type Theory
Version 1.1, defended 19/12/2023
[PDF (French, light mode)] [PDF (French, dark mode)]
[PDF (English, light mode)] [PDF (English, dark mode)]
Publications and presentations:
Trocq: Proof Transfer for Free, With or Without Univalence
with Cyril Cohen and Assia Mahboubi
ESOP 2024 [preprint]
Compositional pre-processing for automated reasoning in dependent type theory
with Valentin Blot, Denis Cousineau, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial
CPP 2023 [DOI] [slides]
Trakt : uniformiser les types pour automatiser les preuves
with Denis Cousineau and Assia Mahboubi
JFLA 2022 [abstract (in French)]