Matthieu Sozeau

36 papers A* 3A 2B 6Journal 19Unranked 4

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Bounded Sort Polymorphism with Elimination Constraints. Proc. ACM Program. Lang. Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter
2025	J	`jnl`	All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. Proc. ACM Program. Lang. Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2025	J	`jnl`	Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. J. ACM Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
2024	J	`jnl`	Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
2021	J	`jnl`	The Marriage of Univalence and Parametricity. J. ACM Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
2021	J	`jnl`	The Multiverse: Logical Modularity for Proof Assistants. CoRR Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2021	—	`conf`	Touring the MetaCoq Project (Invited Paper). LFMTP Matthieu Sozeau
2021	A*	`conf`	Types Are Internal ∞-Groupoids. LICS Eric Finster, Antoine Allioux, Matthieu Sozeau
2021	J	`jnl`	Types are Internal ∞-Groupoids. CoRR Antoine Allioux, Eric Finster, Matthieu Sozeau
2020	J	`jnl`	Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
2020	J	`jnl`	The MetaCoq Project. J. Autom. Reason. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
2019	J	`jnl`	Definitional proof-irrelevance without K. Proc. ACM Program. Lang. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
2019	B	`conf`	Eliminating reflection from type theory. CPP Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
2019	J	`jnl`	Equations reloaded: high-level dependently-typed functional programming and proving in Coq. Proc. ACM Program. Lang. Matthieu Sozeau, Cyprien Mangin
2019	J	`jnl`	The Marriage of Univalence and Parametricity. CoRR Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
2018	B	`conf`	Cumulative Inductive Types In Coq. FSCD Amin Timany, Matthieu Sozeau
2018	J	`jnl`	Equivalences for free: univalent parametricity for effective transport. Proc. ACM Program. Lang. Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
2018	B	`conf`	Towards Certified Meta-Programming with Typed Template-Coq. ITP Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau
2017	J	`jnl`	A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. J. Funct. Program. Beta Ziliani, Matthieu Sozeau
2017	J	`jnl`	Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). CoRR Amin Timany, Matthieu Sozeau
2017	B	`conf`	The HoTT library: a formalization of homotopy type theory in Coq. CPP Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
2016	J	`jnl`	Partiality and recursion in interactive theorem provers - an overview. Math. Struct. Comput. Sci. Ana Bove, Alexander Krauss, Matthieu Sozeau
2016	A*	`conf`	The Definitional Side of the Forcing. LICS Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau
2016	J	`jnl`	The HoTT Library: A formalization of homotopy type theory in Coq. CoRR Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters
2015	—	`ed.`	20th International Conference on Types for Proofs and Programs, TYPES 2014, Paris, France, May 12-15, 2014 TYPES Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau
2015	A	`conf`	A unification algorithm for Coq featuring universe polymorphism and overloading. ICFP Beta Ziliani, Matthieu Sozeau
2015	J	`jnl`	Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study. CoRR Cyprien Mangin, Matthieu Sozeau
2014	—	`conf`	Towards a better-behaved unification algorithm for Coq. UNIF Beta Ziliani, Matthieu Sozeau
2014	B	`conf`	Universe Polymorphism in Coq. ITP Matthieu Sozeau, Nicolas Tabareau
2012	A*	`conf`	Extending Type Theory with Forcing. LICS Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau
2010	B	`conf`	Equations: A Dependent Pattern-Matching Compiler. ITP Matthieu Sozeau
2009	J	`jnl`	A New Look at Generalized Rewriting in Type Theory. J. Formaliz. Reason. Matthieu Sozeau
2008	—	`conf`	First-Class Type Classes. TPHOLs Matthieu Sozeau, Nicolas Oury
2008	—	`—`	Un environnement pour la programmation avec types dépendants. (An environment for programming with dependent types). Matthieu Sozeau
2007	A	`conf`	Program-ing finger trees in Coq. ICFP Matthieu Sozeau
2006	—	`conf`	Subset Coercions in Coq. TYPES Matthieu Sozeau