Matthieu Sozeau

ORCID

Publication Activity (10 Years)

Years Active: 2006-2024
Publications (10 Years): 23

Top Venues

CoRR

Proc. ACM Program. Lang.

ITP

LICS

University of Paris-Sud, Orsay, France (PHD)

Education History

University of Paris-Sud, Orsay, France

PHD

Publications

Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Matthieu Sozeau
Touring the MetaCoq Project (Invited Paper). LFMTP (2021)
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
The Marriage of Univalence and Parametricity. J. ACM 68 (1) (2021)
Antoine Allioux, Eric Finster, Matthieu Sozeau
Types are Internal ∞-Groupoids. CoRR (2021)
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
The Multiverse: Logical Modularity for Proof Assistants. CoRR (2021)
Eric Finster, Antoine Allioux, Matthieu Sozeau
Types Are Internal ∞-Groupoids. LICS (2021)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Matthieu Sozeau, Cyprien Mangin
Equations reloaded: high-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
The Marriage of Univalence and Parametricity. CoRR (2019)
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
Definitional proof-irrelevance without K. Proc. ACM Program. Lang. 3 (POPL) (2019)
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
Eliminating reflection from type theory. CPP (2019)
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Equivalences for free: univalent parametricity for effective transport. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
Towards Certified Meta-Programming with Typed Template-Coq. ITP (2018)
Amin Timany, Matthieu Sozeau
Cumulative Inductive Types In Coq. FSCD (2018)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT library: a formalization of homotopy type theory in Coq. CPP (2017)
Amin Timany, Matthieu Sozeau
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). CoRR (2017)
Beta Ziliani, Matthieu Sozeau
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. J. Funct. Program. 27 (2017)
Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau
The Definitional Side of the Forcing. LICS (2016)
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
The HoTT Library: A formalization of homotopy type theory in Coq. CoRR (2016)
Ana Bove, Alexander Krauss, Matthieu Sozeau
Partiality and recursion in interactive theorem provers - an overview. Math. Struct. Comput. Sci. 26 (1) (2016)
Cyprien Mangin, Matthieu Sozeau
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study. CoRR (2015)
Beta Ziliani, Matthieu Sozeau
A unification algorithm for Coq featuring universe polymorphism and overloading. ICFP (2015)
Matthieu Sozeau, Nicolas Tabareau
Universe Polymorphism in Coq. ITP (2014)
Beta Ziliani, Matthieu Sozeau
Towards a better-behaved unification algorithm for Coq. UNIF (2014)
Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau
Extending Type Theory with Forcing. LICS (2012)
Matthieu Sozeau
Equations: A Dependent Pattern-Matching Compiler. ITP (2010)
Matthieu Sozeau
A New Look at Generalized Rewriting in Type Theory. J. Formaliz. Reason. 2 (1) (2009)
Matthieu Sozeau, Nicolas Oury
First-Class Type Classes. TPHOLs (2008)
Matthieu Sozeau
Program-ing finger trees in Coq. ICFP (2007)
Matthieu Sozeau
Subset Coercions in Coq. TYPES (2006)

Matthieu Sozeau.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Matthieu Sozeau