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
2572008
Subset coercions in Coq
M Sozeau
International Workshop on Types for Proofs and Programs, 237-252, 2006
1152006
A new look at generalized rewriting in type theory
M Sozeau
Journal of formalized reasoning 2 (1), 41-62, 2009
882009
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
692017
Program-ing finger trees in Coq
M Sozeau
Proceedings of the 12th ACM SIGPLAN international conference on Functional …, 2007
682007
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
632017
Universe polymorphism in Coq
M Sozeau, N Tabareau
International Conference on Interactive Theorem Proving, 499-514, 2014
532014
Equations: A dependent pattern-matching compiler
M Sozeau
International Conference on Interactive Theorem Proving, 419-434, 2010
502010
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
462018
Extending type theory with forcing
G Jaber, N Tabareau, M Sozeau
2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 2012
412012
Lecture notes in computer science
G Goos, J Hartmanis
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE, 1984
33*1984
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
312019
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
292016
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
282018
Un environnement pour la programmation avec types dépendants
M Sozeau
Paris 11, 2008
272008
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
242016
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
232019
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
232019
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
232015
The MetaCoq Project
M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ...
Journal of Automated Reasoning, 1-53, 2020
222020
The system can't perform the operation now. Try again later.
Articles 1–20