×
Author ID: sozeau.matthieu Recent zbMATH articles by "Sozeau, Matthieu"
Published as: Sozeau, Matthieu
Homepage: https://www.irif.fr/~sozeau/
External Links: MGP · ORCID · Google Scholar · dblp

Publications by Year

Citations contained in zbMATH Open

15 Publications have been cited 94 times in 81 Documents Cited by Year
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
First-class type classes. Zbl 1165.68475
Sozeau, Matthieu; Oury, Nicolas
23
2008
A new look at generalized rewriting in type theory. Zbl 1205.68364
Sozeau, Matthieu
15
2009
Subset coercions in Coq. Zbl 1178.68531
Sozeau, Matthieu
13
2007
The MetaCoq project. Zbl 1468.68075
Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo
6
2020
Equations: a dependent pattern-matching compiler. Zbl 1291.68369
Sozeau, Matthieu
6
2010
Towards certified meta-programming with typed Template-Coq. Zbl 1468.68071
Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas
5
2018
Partiality and recursion in interactive theorem provers – an overview. Zbl 1361.68186
Bove, Ana; Krauss, Alexander; Sozeau, Matthieu
5
2016
Extending type theory with forcing. Zbl 1364.03016
Jaber, Guilhem; Tabareau, Nicolas; Sozeau, Matthieu
5
2012
Program-ing finger trees in Coq. Zbl 1291.68157
Sozeau, Matthieu
5
2007
Universe polymorphism in Coq. Zbl 1416.68179
Sozeau, Matthieu; Tabareau, Nicolas
4
2014
The definitional side of the forcing. Zbl 1394.68063
Jaber, Guilhem; Lewertowski, Gabriel; Pédrot, Pierre-Marie; Sozeau, Matthieu; Tabareau, Nicolas
3
2016
A unification algorithm for Coq featuring universe polymorphism and overloading. Zbl 1360.68774
Ziliani, Beta; Sozeau, Matthieu
2
2015
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Zbl 1418.68185
Ziliani, Beta; Sozeau, Matthieu
1
2017
Cumulative inductive types in Coq. Zbl 1462.68221
Timany, Amin; Sozeau, Matthieu
1
2018
The MetaCoq project. Zbl 1468.68075
Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo
6
2020
Towards certified meta-programming with typed Template-Coq. Zbl 1468.68071
Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas
5
2018
Cumulative inductive types in Coq. Zbl 1462.68221
Timany, Amin; Sozeau, Matthieu
1
2018
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Zbl 1418.68185
Ziliani, Beta; Sozeau, Matthieu
1
2017
Partiality and recursion in interactive theorem provers – an overview. Zbl 1361.68186
Bove, Ana; Krauss, Alexander; Sozeau, Matthieu
5
2016
The definitional side of the forcing. Zbl 1394.68063
Jaber, Guilhem; Lewertowski, Gabriel; Pédrot, Pierre-Marie; Sozeau, Matthieu; Tabareau, Nicolas
3
2016
A unification algorithm for Coq featuring universe polymorphism and overloading. Zbl 1360.68774
Ziliani, Beta; Sozeau, Matthieu
2
2015
Universe polymorphism in Coq. Zbl 1416.68179
Sozeau, Matthieu; Tabareau, Nicolas
4
2014
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
Extending type theory with forcing. Zbl 1364.03016
Jaber, Guilhem; Tabareau, Nicolas; Sozeau, Matthieu
5
2012
Equations: a dependent pattern-matching compiler. Zbl 1291.68369
Sozeau, Matthieu
6
2010
A new look at generalized rewriting in type theory. Zbl 1205.68364
Sozeau, Matthieu
15
2009
First-class type classes. Zbl 1165.68475
Sozeau, Matthieu; Oury, Nicolas
23
2008
Subset coercions in Coq. Zbl 1178.68531
Sozeau, Matthieu
13
2007
Program-ing finger trees in Coq. Zbl 1291.68157
Sozeau, Matthieu
5
2007
all top 5

Cited by 185 Authors

4 Krebbers, Robbert
4 Tassi, Enrico
3 Birkedal, Lars
3 Cohen, Cyril
3 Jourdan, Jacques-Henri
3 Mahboubi, Assia
3 Pous, Damien
3 Sacerdoti Coen, Claudio
3 Sozeau, Matthieu
3 Spitters, Bas
3 Swierstra, Wouter
2 Abel, Andreas M.
2 Asperti, Andrea
2 Barras, Bruno
2 Bizjak, Aleš
2 Braibant, Thomas
2 Braun, Gabriel
2 Cockx, Jesper
2 Devriese, Dominique
2 Doczkal, Christian
2 Dreyer, Derek R.
2 Forster, Yannick
2 Fürer, Basil
2 Gonthier, Georges
2 Kunčar, Ondřej
2 Kunze, Fabian
2 Lochbihler, Andreas
2 McBride, Conor Thomas
2 Narboux, Julien
2 Ricciotti, Wilmer
2 Sakaguchi, Kazuhiko
2 Schneider, Joshua P.
2 Smolka, Gert
2 Tabareau, Nicolas
2 Théry, Laurent
2 Traytel, Dmitry
2 van der Weegen, Eelis
2 Ziliani, Beta
1 Abrahamsson, Oskar
1 Affeldt, Reynald
1 Ahrens, Benedikt
1 Altenkirch, Thorsten
1 Anand, Abhishek
1 Annenkov, Danil
1 Ayala-Rincón, Mauricio
1 Benton, Nick
1 Bernardo, Bruno
1 Blanqui, Frédéric
1 Botta, Nicola
1 Boulier, Simon
1 Boutry, Pierre
1 Braun, David J.
1 Brede, Nuria
1 Brunel, Aloïs
1 Brunet, Paul
1 Bundy, Alan
1 Cao, Qinxiang
1 Casinghino, Chris
1 Ceulemans, Joris
1 Chakravarty, Manuel M. T.
1 Charguéraud, Arthur
1 Chen, Ran
1 Clouston, Ranald A.
1 Coquand, Thierry
1 Corbineau, Pierre
1 Dagand, Pierre-Evariste
1 de Carvalho-Segundo, Washington
1 Dénès, Maxime
1 Dubois, Catherine
1 Farka, František
1 Feltey, Daniel
1 Fernández, Maribel
1 Fetscher, Burke
1 Findler, Robert Bruce
1 Fisher, Kathleen
1 Frumin, Dan
1 Futatsugi, Kokichi
1 Gaboardi, Marco
1 Garillot, François
1 Ghani, Neil
1 Grathwohl, Hans Bugge
1 Grégoire, Benjamin
1 Grossman, Dan
1 Grov, Gudmund
1 Guan, Yong
1 Guéneau, Armaël
1 Hancock, Peter G.
1 Hanrot, Guillaume
1 Hashimoto, Hideki
1 Herbelin, Hugo
1 Ho, Son Lam
1 Hriţcu, Cătălin
1 Hu, Zhenjiang
1 Huffman, Brian
1 Hur, Chung-Kil
1 Jansson, Patrik
1 Jung, Ralf
1 Kanabar, Hrutvik
1 Keller, Gabriele Cornelia
1 Kennedy, Andrew J.
...and 85 more Authors

Citations by Year