Matthieu Sozeau
Matthieu Sozeau
Resarcher, Inria Paris and PPS
Geverifieerd e-mailadres voor inria.fr
Titel
Geciteerd door
Geciteerd door
Jaar
First-class type classes
M Sozeau, N Oury
International Conference on Theorem Proving in Higher Order Logics, 278-293, 2008
2492008
Subset coercions in Coq
M Sozeau
International Workshop on Types for Proofs and Programs, 237-252, 2006
1092006
A new look at generalized rewriting in type theory
M Sozeau
Journal of formalized reasoning 2 (1), 41-62, 2010
872010
Program-ing finger trees in Coq
M Sozeau
Proceedings of the 12th ACM SIGPLAN international conference on Functional …, 2007
662007
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
632017
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
602017
Universe polymorphism in Coq
M Sozeau, N Tabareau
International Conference on Interactive Theorem Proving, 499-514, 2014
522014
Equations: A dependent pattern-matching compiler
M Sozeau
International Conference on Interactive Theorem Proving, 419-434, 2010
462010
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
392018
Extending type theory with forcing
G Jaber, N Tabareau, M Sozeau
2012 27th Annual IEEE Symposium on Logic in Computer Science, 395-404, 2012
392012
Lecture notes in computer science
G Goos, J Hartmanis
Springer, 1973
32*1973
Un environnement pour la programmation avec types dépendants
M Sozeau
Paris 11, 2008
272008
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
252019
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
252016
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
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
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
222018
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
192019
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
162019
A gentle introduction to type classes and relations in Coq
P Castéran, M Sozeau
Technical Report hal-00702455, version 1, 2012
162012
Het systeem kan de bewerking nu niet uitvoeren. Probeer het later opnieuw.
Artikelen 1–20