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

Observational Equality Meets CIC

Loïc Pujet, Yann Leray, Nicolas Tabareau

ACM Transactions on Programming Languages and Systems (TOPLAS 2025)

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

How (not) to prove typed type conversion transitive

Yann Leray

31st International Conference on Types for Proofs and Programs (TYPES 2025)

Slides Recording