| 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 | 24 | 2024 |
| 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 | 24 | 2022 |
| Complete bidirectional typing for the calculus of inductive constructions M Lennon-Bertrand 12th International Conference on Interactive Theorem Proving (ITP 2021) 193 …, 2021 | 20 | 2021 |
| 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 | 15* | 2025 |
| Bidirectional Typing for the Calculus of Inductive Constructions M Lennon-Bertrand Nantes Université, 2022 | 13 | 2022 |
| Coalgebraic determinization of alternating automata M Bertrand, J Rot arXiv preprint arXiv:1804.02546, 2018 | 11 | 2018 |
| 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 |
| Logical Relation for MLTT in Coq A Adjedj, M Lennon-Bertrand, K Maillard, PM Pédrot, L Pujet | 3 | 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, 37, 2022 | 3 | 2022 |
| 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 | 1 | |
| Equivalence Between Typed and Untyped Conversion Algorithms M Lennon-Bertrand | 1* | |
| What does it take to certify conversion? M Lennon-Bertrand arXiv preprint arXiv:2502.15500, 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 USING NORMALISATION BY EVALUATION M Sirman, MLBN KRISHNASWAMI | | 2024 |
| Definitional Functoriality for Dependent (Sub) Types T Laurent, M Lennon-Bertrand, K Maillard European Symposium on Programming, 302-331, 2024 | | 2024 |
| Definitional Functoriality for Dependent (Sub) Types--Extended version T Laurent, M Lennon-Bertrand, K Maillard arXiv preprint arXiv:2310.14929, 2023 | | 2023 |
| Martin-L\" of\a la Coq A Adjedj, M Lennon-Bertrand, K Maillard, PM Pédrot, L Pujet arXiv preprint arXiv:2310.06376, 2023 | | 2023 |
| 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, 1-3, 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, ... | | |
