I am a PhD student in Gallinette under the supervision of Nicolas Tabareau, Matthieu Sozeau and Théo Winterhalter.

I am mostly interested in formally proving proof assistants correct, including all necessary properties of their underlying type theory. I also wrote the implementation of rewrite rules in Coq, with help from Théo, Gaëtan Gilbert and the rest of the Coq development team.

Publications

Conference papers

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter

International Conference on Interactive Theorem Proving (ITP 2024)

Paper

Talks

The Rewster: The Coq Proof Assistant with Rewrite Rules

Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Winterhalter

29th International Conference on Types for Proofs and Programs (TYPES 2023)

Slides Recording