| 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 | 23 | 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 | 22 | 2024 |
| Complete bidirectional typing for the calculus of inductive constructions M Lennon-Bertrand 12th International Conference on Interactive Theorem Proving (ITP 2021) 193 …, 2021 | 21 | 2021 |
| Coalgebraic determinization of alternating automata M Bertrand, J Rot arXiv preprint arXiv:1804.02546, 2018 | 11 | 2018 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... Journal of the ACM (JACM), 1-76, 2024 | 10* | 2024 |
| Bidirectional Typing for the Calculus of Inductive Constructions M Lennon-Bertrand Nantes Université, 2022 | 10 | 2022 |
| 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 | 8 | 2022 |
| 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 | 3 | 2022 |
| Logical Relation for MLTT in Coq A Adjedj, M Lennon-Bertrand, K Maillard, PM Pédrot, L Pujet | 2 | 2023 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, J Nielsen, N Tabareau, ... Journal of the ACM 72 (1), 1-74, 2025 | | 2025 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq S MATTHIEU, M LENNON-BERTRAND, T WINTERHALTER of the ACM, 1, 2025 | | 2025 |
| Implementing Observational Equality with Normalisation by Evaluation M Sirman, M Lennon-Bertrand, N Krishnaswami 30th International Conference on Types for Proofs and Programs TYPES 2024 …, 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 | | |
