Follow
Matthieu Sozeau
Matthieu Sozeau
Resarcher, Inria Paris and PPS
Verified email at inria.fr
Title
Cited by
Cited by
Year
First-class type classes
M Sozeau, N Oury
International Conference on Theorem Proving in Higher Order Logics, 278-293, 2008
3182008
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
1412017
Subset Coercions in Coq
M Sozeau
International Workshop on Types for Proofs and Programs, 237-252, 2006
1332006
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
1202020
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
1202019
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
1062017
A new look at generalized rewriting in type theory
M Sozeau
Journal of formalized reasoning 2 (1), 41-62, 2009
1012009
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
852019
Universe Polymorphism in Coq
M Sozeau, N Tabareau
International Conference on Interactive Theorem Proving, 499-514, 2014
832014
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
722019
Equations: A dependent pattern-matching compiler
M Sozeau
International Conference on Interactive Theorem Proving, 419-434, 2010
682010
Towards Certified Meta-Programming with Typed Template-Coq
A Anand, S Boulier, C Cohen, M Sozeau, N Tabareau
International Conference on Interactive Theorem Proving, 20-39, 2018
672018
Program-ing finger trees in Coq
M Sozeau
Proceedings of the 12th ACM SIGPLAN international conference on Functional …, 2007
652007
Extending type theory with forcing
G Jaber, N Tabareau, M Sozeau
2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 2012
502012
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
442018
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
362016
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
352016
Eliminating reflection from type theory
T Winterhalter, M Sozeau, N Tabareau
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
342019
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
342015
The marriage of univalence and parametricity
N Tabareau, É Tanter, M Sozeau
Journal of the ACM (JACM) 68 (1), 1-44, 2021
312021
The system can't perform the operation now. Try again later.
Articles 1–20