Meven Lennon-Bertrand

According to our database, Meven Lennon-Bertrand authored at least 15 papers between 2018 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

Bidirectional Interpolation for the Lambda-Calculus - Revisiting and Formalising Craig-Čubrić Interpolation.

Meven Lennon-Bertrand, Alexis Saurin

CoRR, March, 2026

AdapTT: Functoriality for Dependent Type Casts.

Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard

Proc. ACM Program. Lang., 2026

2025

LogRel-Coq - FSCD 2025.

Meven Lennon-Bertrand

Dataset, July, 2025

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter

J. ACM, February, 2025

What does it take to certify conversion?

Meven Lennon-Bertrand

CoRR, February, 2025

What Does It Take to Certify a Conversion Checker?

Meven Lennon-Bertrand

Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction, 2025

2024

Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation.

Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami

Proceedings of the 30th International Conference on Types for Proofs and Programs, 2024

Artifact Description - Definitional Functoriality for Dependent (Sub)Types.

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

Proceedings of the Programming Languages and Systems, 2024

Definitional Functoriality for Dependent (Sub)Types.

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

Proceedings of the Programming Languages and Systems, 2024

Martin-Löf à la Coq.

Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2022

Bidirectional Typing for the Calculus of Inductive Constructions. (Typage Bidirectionnel pour le Calcul des Constructions Inductives).

Meven Lennon-Bertrand

PhD thesis, 2022

Gradualizing the Calculus of Inductive Constructions.

Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter

ACM Trans. Program. Lang. Syst., 2022

A reasonably gradual type theory.

Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter

Proc. ACM Program. Lang., 2022

2021

Complete Bidirectional Typing for the Calculus of Inductive Constructions.

Meven Lennon-Bertrand

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2018

Coalgebraic Determinization of Alternating Automata.

Meven Bertrand, Jurriaan Rot

CoRR, 2018