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
2882008
Subset coercions in Coq
M Sozeau
International Workshop on Types for Proofs and Programs, 237-252, 2006
1232006
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
1032017
A new look at generalized rewriting in type theory
M Sozeau
Journal of formalized reasoning 2 (1), 41-62, 2009
932009
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
842017
Program-ing finger trees in Coq
M Sozeau
Proceedings of the 12th ACM SIGPLAN international conference on Functional …, 2007
752007
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
732019
Universe polymorphism in Coq
M Sozeau, N Tabareau
International Conference on Interactive Theorem Proving, 499-514, 2014
672014
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
662020
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
612019
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
582018
Equations: A dependent pattern-matching compiler
M Sozeau
International Conference on Interactive Theorem Proving, 419-434, 2010
572010
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
522019
Extending type theory with forcing
G Jaber, N Tabareau, M Sozeau
2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 2012
462012
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
392018
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
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
302015
Un environnement pour la programmation avec types dépendants
M Sozeau
Paris 11, 2008
292008
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
272016
Consistency of the predicative calculus of cumulative inductive constructions (pcuic)
A Timany, M Sozeau
arXiv preprint arXiv:1710.03912, 2017
192017
The system can't perform the operation now. Try again later.
Articles 1–20