Matthieu Sozeau

According to our database1, Matthieu Sozeau authored at least 24 papers between 2006 and 2020.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of five.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2020
Coq Coq correct! verification of type checking and erasure for Coq, in Coq.
Proc. ACM Program. Lang., 2020

The MetaCoq Project.
J. Autom. Reason., 2020

2019
Equations reloaded: high-level dependently-typed functional programming and proving in Coq.
Proc. ACM Program. Lang., 2019

Definitional proof-irrelevance without K.
Proc. ACM Program. Lang., 2019

The Marriage of Univalence and Parametricity.
CoRR, 2019

Eliminating reflection from type theory.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018
Equivalences for free: univalent parametricity for effective transport.
Proc. ACM Program. Lang., 2018

Cumulative Inductive Types In Coq.
Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

Towards Certified Meta-Programming with Typed Template-Coq.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading.
J. Funct. Program., 2017

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC).
CoRR, 2017

The HoTT library: a formalization of homotopy type theory in Coq.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016
Partiality and recursion in interactive theorem provers - an overview.
Math. Struct. Comput. Sci., 2016

The Definitional Side of the Forcing.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

2015
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study.
CoRR, 2015

A unification algorithm for Coq featuring universe polymorphism and overloading.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

2014
Universe Polymorphism in Coq.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2012
Extending Type Theory with Forcing.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

2010
Equations: A Dependent Pattern-Matching Compiler.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009
A New Look at Generalized Rewriting in Type Theory.
J. Formaliz. Reason., 2009

2008
Un environnement pour la programmation avec types dépendants. (An environment for programming with dependent types).
PhD thesis, 2008

First-Class Type Classes.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007
Program-ing finger trees in Coq.
Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, 2007

2006
Subset Coercions in Coq.
Proceedings of the Types for Proofs and Programs, International Workshop, 2006


  Loading...