en ¦ fr > Articles

Definitional Functoriality for Dependent (Sub)Types

ESOP 2024
Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard
Pdf Hal

Martin-Löf à la Coq

CPP 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

2023 (Soumis)
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

ICFP 2022
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter
Doi Pdf Hal BibTeX

Gradualizing the Calculus of Inductive Constructions

TOPLAS 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.