Coalgebraic Determinization of Alternating Automata. - Meven Bertrand; Jurriaan Rot (CoRR, 2018)

Complete Bidirectional Typing for the Calculus of Inductive Constructions. - Meven Lennon-Bertrand (ITP, 2021)

A reasonably gradual type theory. - Kenji Maillard; Meven Lennon-Bertrand; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2022)

Gradualizing the Calculus of Inductive Constructions. - Meven Lennon-Bertrand; Kenji Maillard; Nicolas Tabareau; Éric Tanter (ACM Trans. Program. Lang. Syst., 2022)

Bidirectional Typing for the Calculus of Inductive Constructions. (Typage Bidirectionnel pour le Calcul des Constructions Inductives). - Meven Lennon-Bertrand (2022)

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

Definitional Functoriality for Dependent (Sub)Types. - Théo Laurent; Meven Lennon-Bertrand; Kenji Maillard (ESOP (1), 2024)

Artifact Description - Definitional Functoriality for Dependent (Sub)Types. - Théo Laurent; Meven Lennon-Bertrand; Kenji Maillard (ESOP (1), 2024)

Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. - Matthew Sirman; Meven Lennon-Bertrand; Neel Krishnaswami (TYPES, 2024)

What Does It Take to Certify a Conversion Checker? - Meven Lennon-Bertrand (FSCD, 2025)

What does it take to certify conversion? - Meven Lennon-Bertrand (CoRR, 2025)

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. - Matthieu Sozeau; Yannick Forster 002; Meven Lennon-Bertrand; Jakob Botsch Nielsen; Nicolas Tabareau; Théo Winterhalter (J. ACM, 2025)

AdapTT: Functoriality for Dependent Type Casts. - Arthur Adjedj; Meven Lennon-Bertrand; Thibaut Benjamin; Kenji Maillard (CoRR, 2025)