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 Rocq, with help from Théo, Gaëtan Gilbert and the rest of the Rocq development team. I am now maintainer for Rocq’s kernel, especially on matters relating to its guard condition and guard checker.

Publications

Conference papers

Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally

Distinguished Paper

Yann Leray, Théo Winterhalter

Proceedings of the ACM on Programming Languages (POPL 2026)

Paper Artifact

Observational Equality Meets CIC

Loïc Pujet, Yann Leray, Nicolas Tabareau

ACM Transactions on Programming Languages and Systems (TOPLAS 2025)

Paper

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

How (not) to prove typed type conversion transitive

Yann Leray

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

Slides Recording

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