| First-class type classes M Sozeau, N Oury Theorem Proving in Higher Order Logics: 21st International Conference …, 2008 | 299 | 2008 |
| Subset Coercions in Coq M Sozeau Types for Proofs and Programs: International Workshop, TYPES 2006 …, 2007 | 126 | 2007 |
| CertiCoq: A verified compiler for Coq A Anand, A Appel, G Morrisett, Z Paraskevopoulou, R Pollack, ... The third international workshop on Coq for programming languages (CoqPL), 2017 | 109 | 2017 |
| A new look at generalized rewriting in type theory M Sozeau Journal of formalized reasoning 2 (1), 41-62, 2009 | 96 | 2009 |
| The HoTT library: a formalization of homotopy type theory in Coq A Bauer, J Gross, PLF Lumsdaine, M Shulman, M Sozeau, B Spitters Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 90 | 2017 |
| Coq coq correct! verification of type checking and erasure for coq, in coq M Sozeau, S Boulier, Y Forster, N Tabareau, T Winterhalter Proceedings of the ACM on Programming Languages 4 (POPL), 1-28, 2019 | 85 | 2019 |
| The metacoq project M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ... Journal of automated reasoning 64 (5), 947-999, 2020 | 80 | 2020 |
| Universe Polymorphism in Coq M Sozeau, N Tabareau Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | 71 | 2014 |
| Program-ing finger trees in Coq M Sozeau Proceedings of the 12th ACM SIGPLAN international conference on Functional …, 2007 | 69 | 2007 |
| Definitional proof-irrelevance without K G Gilbert, J Cockx, M Sozeau, N Tabareau Proceedings of the ACM on Programming Languages 3 (POPL), 1-28, 2019 | 65 | 2019 |
| Equations reloaded: High-level dependently-typed functional programming and proving in Coq M Sozeau, C Mangin Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019 | 61 | 2019 |
| Equations: A dependent pattern-matching compiler M Sozeau Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010 | 60 | 2010 |
| Towards Certified Meta-Programming with Typed Template-Coq A Anand, S Boulier, C Cohen, M Sozeau, N Tabareau Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018 | 59 | 2018 |
| Extending type theory with forcing G Jaber, N Tabareau, M Sozeau 2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 2012 | 48 | 2012 |
| Equivalences for free: univalent parametricity for effective transport N Tabareau, É Tanter, M Sozeau Proceedings of the ACM on Programming Languages 2 (ICFP), 1-29, 2018 | 40 | 2018 |
| The definitional side of the forcing G Jaber, G Lewertowski, PM Pédrot, M Sozeau, N Tabareau Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer …, 2016 | 36 | 2016 |
| Partiality and recursion in interactive theorem provers–an overview A Bove, A Krauss, M Sozeau Mathematical Structures in Computer Science 26 (1), 38-88, 2016 | 31 | 2016 |
| A unification algorithm for Coq featuring universe polymorphism and overloading B Ziliani, M Sozeau Proceedings of the 20th ACM SIGPLAN International Conference on Functional …, 2015 | 31 | 2015 |
| Un environnement pour la programmation avec types dépendants M Sozeau Paris 11, 2008 | 30 | 2008 |
| Consistency of the predicative calculus of cumulative inductive constructions (pcuic) A Timany, M Sozeau arXiv preprint arXiv:1710.03912, 2017 | 21 | 2017 |
nicolas tabareauInriaVerified email at inria.fr
