en ¦ fr > Publications

AdapTT: Functoriality for Dependent Type Casts

2025 (Soumis)

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

Hal GitHub

What does it take to certify a conversion checker?

Formal Structures for Computation and Deduction, 2025 (Best paper by junior researcher)

Meven Lennon-Bertrand

Doi Pdf ArXiv BibTeX GitHub

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

Types 2024 Post-proceedings, 2025

Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami

Doi Pdf BibTeX GitHub

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

Journal of the ACM, 2025

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

Doi Pdf Hal

Definitional Functoriality for Dependent (Sub)Types

European Symposium on Programming, 2024 (Distinguished artefact)

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

Pdf Hal

Martin-Löf à la Coq

Certified Programs and Proofs, 2024 (Distinguished paper)

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

Doi Pdf Hal ArXiv BibTeX

A Reasonably Gradual Type Theory

International Conference on Functional Programming, 2022

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

Doi Pdf Hal BibTeX

Gradualizing the Calculus of Inductive Constructions

Transactions on Programming Languages and Systems, 2022

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

Présenté à POPL 2022.

Doi Pdf Hal ArXiv BibTeX

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Interactive Theorem Proving, 2021

Meven Lennon-Bertrand

Doi Pdf Hal ArXiv BibTeX

Sous Licence Creative Commons CC0, source sur github. Développé avec Pelican. Thème adapté de pelican-svbhack par Giulio Fidente.