en ¦ fr > Publications

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

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

Journal of the ACM, 2023 (À paraître)

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

In which we report on the MetaCoq project, up to its 1.2 version.

Pdf Hal

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.