Meven Lennon-Bertrand

19 papers B 3Journal 12Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
AdapTT: Functoriality for Dependent Type Casts.
Proc. ACM Program. Lang.
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard
2026 J jnl
Bidirectional Interpolation for the Lambda-Calculus - Revisiting and Formalising Craig-Čubrić Interpolation.
CoRR
Meven Lennon-Bertrand, Alexis Saurin
2025 J jnl
AdapTT: Functoriality for Dependent Type Casts.
CoRR
Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard
2025 J jnl
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.
J. ACM
Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
2025 B conf
What Does It Take to Certify a Conversion Checker?
FSCD
Meven Lennon-Bertrand
2025 J jnl
What does it take to certify conversion?
CoRR
Meven Lennon-Bertrand
2024 — conf
Artifact Description - Definitional Functoriality for Dependent (Sub)Types.
ESOP (1)
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
2024 — conf
Definitional Functoriality for Dependent (Sub)Types.
ESOP (1)
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
2024 — conf
Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation.
TYPES
Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami
2024 B conf
Martin-Löf à la Coq.
CPP
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
2023 J jnl
Definitional Functoriality for Dependent (Sub)Types.
CoRR
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
2023 J jnl
Martin-Löf à la Coq.
CoRR
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
2022 J jnl
A Reasonably Gradual Type Theory.
CoRR
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
2022 J jnl
A reasonably gradual type theory.
Proc. ACM Program. Lang.
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
2022 — —
Bidirectional Typing for the Calculus of Inductive Constructions. (Typage Bidirectionnel pour le Calcul des Constructions Inductives).
Meven Lennon-Bertrand
2022 J jnl
Gradualizing the Calculus of Inductive Constructions.
ACM Trans. Program. Lang. Syst.
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
2021 B conf
Complete Bidirectional Typing for the Calculus of Inductive Constructions.
ITP
Meven Lennon-Bertrand
2021 J jnl
Complete Bidirectional Typing for the Calculus of Inductive Constructions.
CoRR
Meven Lennon-Bertrand
2020 J jnl
Gradualizing the Calculus of Inductive Constructions.
CoRR
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter