Matthieu Sozeau
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
10
Venues
4
Active years
2007–2021
Best venue rank
A*
Where they publish
Papers
10 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2021 | LICS | Types Are Internal ∞-Groupoids. | Eric Finster, Antoine Allioux, Matthieu Sozeau |
| 2019 | CPP | Eliminating reflection from type theory. | Tho Winterhalter, Matthieu Sozeau, Nicolas Tabareau |
| 2018 | ITP | Towards Certified Meta-Programming with Typed Template-Coq. | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
| 2017 | CPP | The HoTT library: a formalization of homotopy type theory in Coq. | Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters |
| 2016 | LICS | The Definitional Side of the Forcing. | Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pdrot, Matthieu Sozeau, Nicolas Tabareau |
| 2015 | ICFP | A unification algorithm for Coq featuring universe polymorphism and overloading. | Beta Ziliani, Matthieu Sozeau |
| 2014 | ITP | Universe Polymorphism in Coq. | Matthieu Sozeau, Nicolas Tabareau |
| 2012 | LICS | Extending Type Theory with Forcing. | Guilhem Jaber, Nicolas Tabareau, Matthieu Sozeau |
| 2010 | ITP | Equations: A Dependent Pattern-Matching Compiler. | Matthieu Sozeau |
| 2007 | ICFP | Program-ing finger trees in Coq. | Matthieu Sozeau |