Matthieu Sozeau
Matthieu Sozeau
Resarcher, Inria Paris and PPS
Verified email at
Cited by
Cited by
First-class type classes
M Sozeau, N Oury
Theorem Proving in Higher Order Logics: 21st International Conference …, 2008
Subset Coercions in Coq
M Sozeau
Types for Proofs and Programs: International Workshop, TYPES 2006 …, 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
A new look at generalized rewriting in type theory
M Sozeau
Journal of formalized reasoning 2 (1), 41-62, 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
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
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
Program-ing finger trees in Coq
M Sozeau
Proceedings of the 12th ACM SIGPLAN international conference on Functional …, 2007
Universe Polymorphism in Coq
M Sozeau, N Tabareau
Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014
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
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
Equations: A dependent pattern-matching compiler
M Sozeau
Interactive Theorem Proving: First International Conference, ITP 2010 …, 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
Extending type theory with forcing
G Jaber, N Tabareau, M Sozeau
2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 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
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
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
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
Un environnement pour la programmation avec types dépendants
M Sozeau
Paris 11, 2008
Consistency of the predicative calculus of cumulative inductive constructions (pcuic)
A Timany, M Sozeau
arXiv preprint arXiv:1710.03912, 2017
The system can't perform the operation now. Try again later.
Articles 1–20