The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. - Yann Leray; Gaëtan Gilbert; Nicolas Tabareau; Théo Winterhalter (ITP, 2024)

Observational Equality Meets CIC. - Loïc Pujet; Yann Leray; Nicolas Tabareau (ACM Trans. Program. Lang. Syst., 2025)