Activity 🧐
PhD subject
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 was 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. Then, I focused 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 wrote 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.
Scientific contributions
PhD thesis:
- 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)]
Software:
Trocq
Parametricity plugin for Coq
[website repository]Trakt
Goal preprocessing plugin for Coq
[website] [repository]
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: a generic pre-processing tactic for theory-based proof automation
with Denis Cousineau and Assia Mahboubi
Coq Workshop 2022 [abstract] [slides] [video]Trakt : uniformiser les types pour automatiser les preuves
with Denis Cousineau and Assia Mahboubi
JFLA 2022 [abstract (in French)]
Teaching
Constraint programming
12h of lectures, 14h of practical sessions
2023, INSA RennesAdvanced algorithms
~30h of practical sessions
2021, IUT of Nantes (website in French)