| Gradualizing the Calculus of Inductive Constructions M Lennon-Bertrand, K Maillard, N Tabareau, É Tanter ACM Transactions on Programming Languages and Systems (TOPLAS) 44 (2), 1-82, 2022 | 20 | 2022 |
| Complete bidirectional typing for the calculus of inductive constructions M Lennon-Bertrand 12th International Conference on Interactive Theorem Proving (ITP 2021) 193 …, 2021 | 18 | 2021 |
| Coalgebraic determinization of alternating automata M Bertrand, J Rot arXiv preprint arXiv:1804.02546, 2018 | 11 | 2018 |
| Bidirectional Typing for the Calculus of Inductive Constructions M Lennon-Bertrand Nantes Université, 2022 | 8 | 2022 |
| Martin-Löf à la Coq A Adjedj, M Lennon-Bertrand, K Maillard, PM Pédrot, L Pujet Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024 | 7 | 2024 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... | 7 | 2023 |
| A reasonably gradual type theory K Maillard, M Lennon-Bertrand, N Tabareau, É Tanter Proceedings of the ACM on Programming Languages 6 (ICFP), 931-959, 2022 | 4 | 2022 |
| Logical Relation for MLTT in Coq A Adjedj, M Lennon-Bertrand, K Maillard, PM Pédrot, L Pujet | 2 | 2023 |
| The Curious Case of Case: Correct & Efficient Representation of Case Analysis in Coq and MetaCoq M Sozeau, M Lennon-Bertrand, Y Forster Talk. 1st Workshop on the Implementation of Type Systems, 2022 | 2 | 2022 |
| Artifact Description: Definitional Functoriality for Dependent (Sub) Types T Laurent, M Lennon-Bertrand, K Maillard European Symposium on Programming, 332-337, 2024 | | 2024 |
| Definitional Functoriality for Dependent (Sub) Types T Laurent, M Lennon-Bertrand, K Maillard European Symposium on Programming, 302-331, 2024 | | 2024 |
| Engineering logical relations for MLTT in Coq A Adjedj, M Lennon-Bertrand, K Maillard, L Pujet TYPES 2023-29th International Conference on Types for Proofs and Programs, 2023 | | 2023 |
| Compilation of Dependently Typed Pattern-Matching for Coq M Bertrand, H Herbelin | | 2016 |
| Projects in the MetaCoq ecosystem Y Forster, M Lennon-Bertrand, K Maillard, PM Pédrot, K Sakaguchi, ... | | |
| Denotational Semantics M Lennon-Bertrand | | |
| A SHINY HAMMER AND MANY THINGS TO HIT M LENNON-BERTRAND | | |
| Decidable Type-Checking for Bidirectional Martin-Löf Type Theory M Lennon-Bertrand, N Krishnaswami 29th International Conference on Types for Proofs and Programs TYPES 2023 …, 0 | | |
| Equivalence Between Typed and Untyped Conversion Algorithms M Lennon-Bertrand | | |
