Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

6 résultats
Image document

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Meven Lennon-Bertrand
ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome, Italy. pp.1-19, ⟨10.4230/LIPIcs.ITP.2021.24⟩
Communication dans un congrès hal-03139924v2
Image document

Bidirectional Typing for the Calculus of Inductive Constructions

Meven Lennon-Bertrand
Autre [cs.OH]. Nantes Université, 2022. Français. ⟨NNT : 2022NANU4033⟩
Thèse tel-03848595v2
Image document

Martin-Löf à la Coq

Arthur Adjedj , Meven Lennon-Bertrand , Kenji Maillard , Pierre-Marie Pédrot , Loïc Pujet
2024
Pré-publication, Document de travail hal-04214008v2
Image document

Gradualizing the Calculus of Inductive Constructions

Meven Lennon-Bertrand , Kenji Maillard , Nicolas Tabareau , Éric Tanter
ACM Transactions on Programming Languages and Systems (TOPLAS), 2022, ⟨10.1145/3495528⟩
Article dans une revue hal-02896776v5
Image document

A Reasonably Gradual Type Theory

Kenji Maillard , Meven Lennon-Bertrand , Nicolas Tabareau , Éric Tanter
Proceedings of the ACM on Programming Languages, In press
Article dans une revue hal-03596652v2
Image document

Definitional Functoriality for Dependent (Sub)Types

Théo Laurent , Meven Lennon-Bertrand , Kenji Maillard
2023
Pré-publication, Document de travail hal-04160858v3