Subset Coercions in Coq. - Matthieu Sozeau (TYPES, 2006)

Program-ing finger trees in Coq. - Matthieu Sozeau (ICFP, 2007)

First-Class Type Classes. - Matthieu Sozeau; Nicolas Oury (TPHOLs, 2008)

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

A New Look at Generalized Rewriting in Type Theory. - Matthieu Sozeau (J. Formaliz. Reason., 2009)

Equations: A Dependent Pattern-Matching Compiler. - Matthieu Sozeau (ITP, 2010)

Extending Type Theory with Forcing. - Guilhem Jaber; Nicolas Tabareau; Matthieu Sozeau (LICS, 2012)

Universe Polymorphism in Coq. - Matthieu Sozeau; Nicolas Tabareau (ITP, 2014)

Towards a better-behaved unification algorithm for Coq. - Beta Ziliani; Matthieu Sozeau (UNIF, 2014)

A unification algorithm for Coq featuring universe polymorphism and overloading. - Beta Ziliani; Matthieu Sozeau (ICFP, 2015)

Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study. - Cyprien Mangin; Matthieu Sozeau (CoRR, 2015)

The Definitional Side of the Forcing. - Guilhem Jaber; Gabriel Lewertowski; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau (LICS, 2016)

Partiality and recursion in interactive theorem provers - an overview. - Ana Bove; Alexander Krauss 001; Matthieu Sozeau (Math. Struct. Comput. Sci., 2016)

The HoTT library: a formalization of homotopy type theory in Coq. - Andrej Bauer; Jason Gross; Peter LeFanu Lumsdaine; Michael Shulman; Matthieu Sozeau; Bas Spitters (CPP, 2017)

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). - Amin Timany; Matthieu Sozeau (CoRR, 2017)

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. - Beta Ziliani; Matthieu Sozeau (J. Funct. Program., 2017)

Towards Certified Meta-Programming with Typed Template-Coq. - Abhishek Anand; Simon Boulier; Cyril Cohen; Matthieu Sozeau; Nicolas Tabareau (ITP, 2018)

Cumulative Inductive Types In Coq. - Amin Timany; Matthieu Sozeau (FSCD, 2018)

Equivalences for free: univalent parametricity for effective transport. - Nicolas Tabareau; Éric Tanter; Matthieu Sozeau (Proc. ACM Program. Lang., 2018)

Eliminating reflection from type theory. - Théo Winterhalter; Matthieu Sozeau; Nicolas Tabareau (CPP, 2019)

Definitional proof-irrelevance without K. - Gaëtan Gilbert; Jesper Cockx; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2019)

Equations reloaded: high-level dependently-typed functional programming and proving in Coq. - Matthieu Sozeau; Cyprien Mangin (Proc. ACM Program. Lang., 2019)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

Coq Coq correct! verification of type checking and erasure for Coq, in Coq. - Matthieu Sozeau; Simon Boulier; Yannick Forster 002; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2020)

Types Are Internal ∞-Groupoids. - Eric Finster; Antoine Allioux; Matthieu Sozeau (LICS, 2021)

Touring the MetaCoq Project (Invited Paper). - Matthieu Sozeau (LFMTP, 2021)

The Multiverse: Logical Modularity for Proof Assistants. - Kenji Maillard; Nicolas Margulies; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (CoRR, 2021)

The Marriage of Univalence and Parametricity. - Nicolas Tabareau; Éric Tanter; Matthieu Sozeau (J. ACM, 2021)

Verified Extraction from Coq to OCaml. - Yannick Forster 002; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2024)

All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. - Josselin Poiret; Gaëtan Gilbert; Kenji Maillard; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2025)

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. - Matthieu Sozeau; Yannick Forster 002; Meven Lennon-Bertrand; Jakob Botsch Nielsen; Nicolas Tabareau; Théo Winterhalter (J. ACM, 2025)