Cubical synthetic homotopy theory. - Anders Mörtberg; Loïc Pujet (CPP, 2020)

Observational equality: now for good. - Loïc Pujet; Nicolas Tabareau (Proc. ACM Program. Lang., 2022)

Computing with Extensionality Principles in Type Theory. (Calculer avec des Principes d'Extensionnalité en Théorie des Types). - Loïc Pujet (2022)

Impredicative Observational Equality. - Loïc Pujet; Nicolas Tabareau (Proc. ACM Program. Lang., 2023)

Martin-Löf à la Coq. - Arthur Adjedj; Meven Lennon-Bertrand; Kenji Maillard; Pierre-Marie Pédrot; Loïc Pujet (CPP, 2024)

Observational Equality Meets CIC. - Loïc Pujet; Nicolas Tabareau (ESOP (1), 2024)

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