en ¦ fr > Publications

What does it take to certify conversion

2025 (Soumis)

Meven Lennon-Bertrand

Pdf ArXiv

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

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

Pdf Hal

Martin-Löf à la Coq

Certified Programs and Proofs, 2024 (Article distingué)

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.