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:

Software:

Publications and presentations:

Teaching