Matthieu Sozeau

According to our database, Matthieu Sozeau authored at least 29 papers between 2006 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Verified Extraction from Coq to OCaml.

Yannick Forster, Matthieu Sozeau, Nicolas Tabareau

Proc. ACM Program. Lang., 2024

2021

The Marriage of Univalence and Parametricity.

Nicolas Tabareau, Éric Tanter, Matthieu Sozeau

J. ACM, 2021

The Multiverse: Logical Modularity for Proof Assistants.

Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter

CoRR, 2021

Touring the MetaCoq Project (Invited Paper).

Matthieu Sozeau

Proceedings of the Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2021

Types Are Internal ∞-Groupoids.

Eric Finster, Antoine Allioux, Matthieu Sozeau

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Coq Coq correct! verification of type checking and erasure for Coq, in Coq.

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter

Proc. ACM Program. Lang., 2020

The MetaCoq Project.

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter

J. Autom. Reason., 2020

2019

Equations reloaded: high-level dependently-typed functional programming and proving in Coq.

Matthieu Sozeau, Cyprien Mangin

Proc. ACM Program. Lang., 2019

Definitional proof-irrelevance without K.

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau

Proc. ACM Program. Lang., 2019

Eliminating reflection from type theory.

Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Equivalences for free: univalent parametricity for effective transport.

Nicolas Tabareau, Éric Tanter, Matthieu Sozeau

Proc. ACM Program. Lang., 2018

Cumulative Inductive Types In Coq.

Amin Timany, Matthieu Sozeau

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

Towards Certified Meta-Programming with Typed Template-Coq.

Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau

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.

Beta Ziliani, Matthieu Sozeau

J. Funct. Program., 2017

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

Amin Timany, Matthieu Sozeau

CoRR, 2017

The HoTT library: a formalization of homotopy type theory in Coq.

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Partiality and recursion in interactive theorem provers - an overview.

Ana Bove, Alexander Krauss, Matthieu Sozeau

Math. Struct. Comput. Sci., 2016

The Definitional Side of the Forcing.

Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau

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.

Cyprien Mangin, Matthieu Sozeau

CoRR, 2015

A unification algorithm for Coq featuring universe polymorphism and overloading.

Beta Ziliani, Matthieu Sozeau

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

2014

Towards a better-behaved unification algorithm for Coq.

Beta Ziliani, Matthieu Sozeau

Proceedings of the 28th International Workshop on Unification, 2014

Universe Polymorphism in Coq.

Matthieu Sozeau, Nicolas Tabareau

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2012

Extending Type Theory with Forcing.

Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

2010

Equations: A Dependent Pattern-Matching Compiler.

Matthieu Sozeau

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

A New Look at Generalized Rewriting in Type Theory.

Matthieu Sozeau

J. Formaliz. Reason., 2009

2008

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

Matthieu Sozeau

PhD thesis, 2008

First-Class Type Classes.

Matthieu Sozeau, Nicolas Oury

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007

Program-ing finger trees in Coq.

Matthieu Sozeau

Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, 2007

2006

Subset Coercions in Coq.

Matthieu Sozeau

Proceedings of the Types for Proofs and Programs, International Workshop, 2006