Matthieu Sozeau :: Curriculum Vitæ

Curriculum Vitæ

Pdf version.

Matthieu Sozeau

Adress:

8 rue Jean Poulain
44300 Nantes
France

Phone:

(+33) 6 88 36 74 27

Email:

matthieu.sozeau@inria.fr

Website:

https://sozeau.gitlabpages.inria.fr/www/

Projects and Grants

Coordinator of the Rocq development team since 2016 and major contributor to Rocq since 2005.
Lead developer of the Equations plugin and the MetaRocq project.
Member of the CertiCoq project, led by Andrew Appel at Princeton University.
ERC Starting Grant CoqHoTT led by Nicolas Tabareau (Inria Rennes, École des Mines de Nantes), 2015-2020. Collaborator.

Jobs, visits and internships

Since December 2019:
INRIA Nantes, Gallinette team -
Researcher (CRCN).
June-July 2019:
University of Pennsylvania, Philadelphia, PA, USA -
Visit of the NSF DeepSpec project.
September-December 2012:
Institute for Advanced Study, Princeton, NJ, USA -
Member of the Univalent Foundations program.
October 2010 - December 2019:
INRIA Paris, pi.r2 team -
Junior Researcher (CRCN).
March 2009 - September 2010:
Harvard University -
Postdoctoral Fellow.
September to December 2008:
Paris XI University -
Temporary researcher at CNRS.
2005-2008:
Paris XI University -
PhD Thesis funded by the french government.
2005-2008:
Paris XI University -
Teaching assistant position in Computer Science.
March to September 2005:
Paris XI University -
Master internship on the development of an environment for programming with dependent types.
Under the direction of
Christine Paulin-Mohring
.

Education

2009-10:
Harvard University
-
Postdoctoral studies in the Ynot group.
Working with Greg Morrisett and his team on Coq and Ynot.
2005-08:
Paris XI University
-
PhD in Computer Science.
With honors.
2004-05:
Paris VII University - Denis Diderot
-
Master of research in Computer Science.
Grade A.
2003-04:
Paris XI University
-
"Maitrise" of Computer Science.
Grade B.
2002-03:
Paris XI University
-
Licence in Computer Science.
Grade B.
2000-02:
Orsay's Institute of Technology
-
University Diploma of Technology in Computer Science.
Grade B.

Books

Homotopy Type Theory: Univalent Foundations for Mathematics. The Univalent Foundations Program. Institute for Advanced Study, 2013.

Journals

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. Sozeau, Matthieu, Forster, Yannick, Lennon-Bertrand, Meven, Nielsen, Jakob, Tabareau, Nicolas & Winterhalter, Théo J. ACM 72 (1), January 2025.
DOI
Verified Extraction from Coq to OCaml. Yannick Forster, Matthieu Sozeau & Nicolas Tabareau Proc. ACM Program. Lang. 8 (PLDI), 2024, pp.52-75.
DOI
The Marriage of Univalence and Parametricity. Tabareau, Nicolas, Tanter, Éric & Sozeau, Matthieu J. ACM 68 (1), January 2021.
DOI
Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau & Théo Winterhalter Proceedings of the ACM on Programming Languages 4 (POPL), January 2020.
DOI
The MetaCoq Project. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau & Théo Winterhalter Journal of Automated Reasoning 64 (5), 2020, pp.947-999.
DOI
Equations Reloaded: High-Level Dependently-Typed Programming and Proving in Coq. Matthieu Sozeau & Cyprien Mangin PACMPL 3 (ICFP), August 2019, pp.86-115.
DOI
Definitional Proof-Irrelevance without K in 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Gilbert, Gaëtan, Cockx, Jesper, Sozeau, Matthieu & Tabareau, Nicolas. Lisbon, Portugal, January 2019.
Equivalences for free: univalent parametricity for effective transport. Nicolas Tabareau, Éric Tanter & Matthieu Sozeau PACMPL 2 (ICFP), 2018, pp.92:1-92:29.
DOI
A Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading. Beta Ziliani & Matthieu Sozeau Journal of Functional Programming 27, 2017, p.e10.
DOI
Partiality and recursion in interactive theorem provers - an overview. Ana Bove, Alexander Krauss & Matthieu Sozeau Mathematical Structures in Computer Science FirstView, 2 2015, pp.1-51.
DOI
A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau Journal of Formalized Reasoning 2 (1), December 2009, pp.41-62.

International Conferences

Types are Internal $\infty$-groupoids. Antoine Allioux, Eric Finster & Matthieu Sozeau LICS, January 2021.
Eliminating reflection from type theory in Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. Théo Winterhalter, Matthieu Sozeau & Nicolas Tabareau. , 2019, pp.91-103.
DOI
Cumulative Inductive Types In Coq in FSCD. Amin Timany & Matthieu Sozeau. , July 2018, pp.29:1-29:16.
DOI
Towards Certified Meta-Programming with Typed Template-Coq in ITP 2018. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau & Nicolas Tabareau. Springer, July 2018, pp.20-39.
DOI
The HoTT library: a formalization of homotopy type theory in Coq in Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau & Bas Spitters. ACM, 2017, pp.164-172.
DOI
The Definitional Side of the Forcing in LICS '16. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau. , 2016, pp.367-376.
DOI
A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading in ACM SIGPLAN International Conference on Functional Programming 2015. Beta Ziliani & Matthieu Sozeau. , 2015.
Universe Polymorphism in Coq in ITP 2014. Matthieu Sozeau & Nicolas Tabareau. , 2014, pp.499-514.
DOI
Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem, Tabareau, Nicolas & Sozeau, Matthieu. Dubrovnik, Croatie, June 2012.
Equations: A Dependent Pattern-Matching Compiler in First International Conference on Interactive Theorem Proving. Matthieu Sozeau. Springer, July 2010.
slides
First-Class Type Classes in TPHOLs. Matthieu Sozeau & Nicolas Oury. Otmane Ait Mohamed, César Muñoz and Sofiène Tahar (Eds). Volume 5170 of LNCS. Springer, August 2008, pp.278-293.
© Springer
DOI
slides
(18/40)
Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau. Freiburg, Germany: ACM Press, 2007, pp.13-24.
© ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'07, http://doi.acm.org/10.1145/1291151.1291156
DOI
slides
(26/103)
Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
© Springer
DOI
slides
(17/29)

International Workshops

Touring the MetaCoq Project in LFMTP 2021. Matthieu Sozeau. Online, July 2021 - Invited paper.
Coq Coq Codet! Towards a Verified Toolchain for Coq in MetaCoq. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau & Théo Winterhalter, Misc, July 2019.
Nested, Well-Founded and Mutual recursion in Equations. Matthieu Sozeau, Talk given at the EUTypes 2018 Working Meeting, Nijmegen, Netherlands, January 2018.
Typed Template Coq in CoqPL'18. Simon Boulier, Matthieu Sozeau, Nicolas Tabareau & Abhishek Anand. Los Angeles, CA, USA, January 2018.
CertiCoq: A verified compiler for Coq in CoqPL. Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau & Matthew Weaver. Paris, France, January 2017.
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study in Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice. Mangin, Cyprien & Sozeau, Matthieu. Volume 185 of EPTCS. , May 2015 - LFMTP'15.
DOI
A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau 1st Coq Workshop proceedings, August 2009.
slides

National Conferences

Classes de types de première classe in Journées Nationales du GDR GPL. Matthieu Sozeau & Nicolas Oury. Toulouse, France, January 2009.
slides

Theses

Un environnement pour la programmation avec types dépendants. Matthieu Sozeau, PhD Thesis, Université Paris 11, Orsay, France, December 2008.
slides
Coercion par prédicats en Coq. Matthieu Sozeau, Master's Thesis, Université Paris VII, LRI, Orsay, 2005.

Research Reports

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Timany, Amin & Sozeau, Matthieu, Technical Report, KU Leuven, Belgium ; Inria Paris, October 2017, p.30.

Software

mattam82/Coq-Equations: Equations 1.3 for Coq 8.17, version v1.3-8.17. Matthieu Sozeau, Pierre-Marie Pédrot, Cyprien Mangin, Gaëtan Gilbert, Emilio Jes\'us Gallego Arias, Hugo Herbelin, Maxime Dénès, Robin Green, Enrico Tassi, Guillaume Claret, Siddharth, Anton Trunov, Jim Fehrle, Joachim Breitner, Karl Palmskog, Kenji Maillard, antonio nikishaev, John Wiegley, SimonBoulier, Søren Nørb\aek, Théo Zimmermann, Vincent Laporte & Yves Bertot, January 2023.
DOI
MetaCoq/metacoq: MetaCoq 1.1.1 for Coq 8.16, version v1.1.1-8.16. Matthieu Sozeau, Théo Winterhalter, SimonBoulier, Yannick Forster, Abhishek Anand, Meven Lennon-Bertrand, nicolas tabareau, Gregory Malecha, Jakob Botsch Nielsen, Pierre-Marie Pédrot, Kenji Maillard, Danil Annenkov, Gaëtan Gilbert, Hugo Herbelin, Marcel Ullrich, Enrico Tassi, yannl35133, Gabriel Scherer, Maxime Dénès, Fabian Kunze, Jason Gross, Pierre Roux, Emilio Jes\'us Gallego Arias, Lo\"\ic, Jim Fehrle, Julin S, Karl Palmskog, Vincent Laporte, Lucas Escot & Xia Li-yao, October 2022.
DOI
Equations, version 1.3. Matthieu Sozeau, January 2022.
DOI
Equations, version 1.0. Matthieu Sozeau & Cyprien Mangin, December 2017.
DOI
The Coq Proof Assistant, version 8.16. The Coq Development Team, September 2022.
DOI
The Coq Proof Assistant, version 8.15. The Coq Development Team, January 2022.
DOI
The Coq Proof Assistant, version 8.14. The Coq Development Team, October 2021.
DOI
The Coq Proof Assistant, version 8.13. The Coq Development Team, January 2021.
DOI
The Coq Proof Assistant, version 8.12. The Coq Development Team, July 2020.
DOI
The Coq Proof Assistant, version 8.11. The Coq Development Team, January 2020.
DOI
The Coq Proof Assistant, version 8.10. The Coq Development Team, October 2019.
DOI
The Coq Proof Assistant, version 8.9. The Coq Development Team, January 2019.
DOI
The Coq Proof Assistant, version 8.8.0. The Coq Development Team, Apr 2018.
DOI
The Coq Proof Assistant, version 8.7.1. The Coq Development Team, December 2017.
DOI
The Coq Proof Assistant, version 8.6. The Coq Development Team, December 2016.
The Coq Proof Assistant, version 8.5. The Coq Development Team, January 2016.
The Coq Proof Assistant, version 8.4. The Coq Development Team, January 2012.
The Coq Proof Assistant, version 8.3. The Coq Development Team, October 2010.
The Coq Proof Assistant, version 8.2. The Coq Development Team, October 2009.
The Coq Proof Assistant, version 8.1. The Coq Development Team, October 2006.

Manuals and Tutorials

A Gentle Introduction to Type Classes and Rewriting in Coq. Pierre Castéran & Matthieu Sozeau, Misc, May 2012.
`Type Classes' in Coq Reference Manual. Matthieu Sozeau. Inria, 2008-2018.
`User defined equalities and relations' in Coq Reference Manual. Matthieu Sozeau. Inria, 2008-2018.
`Program' in Coq Reference Manual. Matthieu Sozeau. Inria, 2008-2018.

Invited Talks and Seminars

MetaCoq: Towards a Certified Kernel and Extraction for Coq. Matthieu Sozeau, Invited talk at JFLAs 2024, Saint-Jacut-de-la-Mer, France. Animated HTML version., January 31st 2024.
Touring the MetaCoq Project. Matthieu Sozeau, Invited talk at LFMTP'21, July 2021.
Coq Development. Matthieu Sozeau, Talk given at the 2021 Coq Workshop, Online, July 2021.
Coq Coq Correct!. Matthieu Sozeau & Théo Winterhalter, Talk given at the Cambium Seminar, February 2021.
Coq Development in CoqPL'21. Matthieu Sozeau & Enrico Tassi. Online, January 2021.
Coq Development in CoqPL'20. Maxime Dénès & Matthieu Sozeau. New Orleans, LA, USA, January 2020.
Coq Development in CoqPL'19. Maxime Dénès & Matthieu Sozeau. Cascais, Portugal, January 2019.
The Predicative, Polymorphic, Cumulative Calculus of Inductive Constructions and its implementation. Matthieu Sozeau, Invited talk at the TYPES 2018 conference, Braga, Portugal, June 20th 2018.
Coq dev talk in CoqPL'18. Matthieu Sozeau, Maxime Dénès & Yves Bertot. Los Angeles, CA, USA, January 2018.
Coq Development in CoqPL'17. Matthieu Sozeau. Paris, France, January 2017.
Coq 8.6. Matthieu Sozeau, Talk at the Coq Workshop in Nancy, France, August 26th 2016.
Forcing Translations in Type Theory. Matthieu Sozeau, Invited talk at the Categorical Logic and Univalent Foundations workshop, Leeds, UK, July 28th 2016.
Coq for HoTT. Matthieu Sozeau, Invited talk at the International Conference on Mathematical Software in Berlin, Germany, July 14th 2016.
Coq 8.6. Maxime Dénès, Matthieu Sozeau, Talk at the DeepSpec Kickoff Workshop in Princeton, NJ, USA, June 8th 2016.
Coq 8.5 at work. Maxime Dénès, Matthieu Sozeau, Talk given at the second CoqPL Workshop, St Petersburg, FL, January 2016.
Equations: a function definition toolbox for Coq. Matthieu Sozeau, Talk at Dagstuhl, March 2016.
Coq - Recent History. Matthieu Sozeau, SIGPLAN Programming Language Software Award 2013 talk, at POPL'14, San Diego, January 23rd 2014.
Coq with Classes. Matthieu Sozeau, Lecture at the "Advanced Martial Arts in Coq" course at University of Pennsylvania, October 2012.
Coq with Classes. Matthieu Sozeau, Talk given at the IAS seminar in Princeton, NJ, October 2012.
Equations: A Dependent Pattern-Matching Suite. Matthieu Sozeau, Talk given at the Institute of Cybernetics, Tallinn, Estonia, May 2012.
Coq with Classes. Matthieu Sozeau, Lecture notes for a course given at JFLA'12 in Carnac, France, February 2012.
Coq with Classes. Matthieu Sozeau, Talk given at the PLAS seminar in Canterbury - UK, November 2011.
Coq with Classes. Matthieu Sozeau, Talk given at the IMDEA seminar in Madrid - Spain, October 2011.
Coq with Classes. Matthieu Sozeau, Talk given at the PPS days in Trouville - France, September 2011.
Equations: A Dependent Pattern-Matching Suite. Matthieu Sozeau, Talk given at the DTP meeting in Shonan - Japan, September 2011.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at University of Chalmers - Gothenburg, January 2011.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at the University of Pennsylvania PLClub, September 2010.
Elaborations in Type Theory. Matthieu Sozeau, Invited Talk at DTP'10 - Edinburgh, UK, July 2010.
Equations: A Dependent Pattern-Matching Compiler. Matthieu Sozeau, Talk given at PPS - Université Paris 7, January 2010.
Programming with Dependent Types in Coq. Matthieu Sozeau, PPS Seminar, Paris, France, 26th February 2009.
An Environment for Proving and Programming. Matthieu Sozeau, LIFO Seminar, Orléans, France, 26th January 2009.
An Environment for Programming with Dependent Types. Matthieu Sozeau, ICIS Seminar, Nijmegen, Netherlands, 20th January 2009.
First-Class Type Classes. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 3rd November 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at the Foundations of Programming seminar, Nottingham, UK, 15th February 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at Harvard, Cambridge, MA, 23th january 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at Portland State University, Portland, OR, 16th january 2008.
Program-ing in Coq. Matthieu Sozeau, Talk given at the Gallium seminar, Rocquencourt, 16th march 2007.

Hobbies

Music: Guitar, Bass and Drums.
Dance: Forró and Lindy-Hop

Higher Structures in Homotopy Type Theory. Antoine Allioux, PhD Thesis, Université de Paris, 2023.

Types are Internal $\infty$-groupoids. Antoine Allioux, Eric Finster & Matthieu Sozeau LICS, January 2021.

A Restricted Version of Reflection Compatible with Univalent Homotopy Type Theory. Winterhalter, Théo, Master's Thesis, ENS Cachan, September 2017.

Formalisation and Meta-Theory of Type Theory. Winterhalter, Théo, PhD Thesis, Université de Nantes, 2020 - 2020NANT4012.

Eliminating reflection from type theory in Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019. Théo Winterhalter, Matthieu Sozeau & Nicolas Tabareau. , 2019, pp.91-103.

DOI

Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau & Théo Winterhalter Proceedings of the ACM on Programming Languages 4 (POPL), January 2020.

DOI

The MetaCoq Project. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau & Théo Winterhalter Journal of Automated Reasoning 64 (5), 2020, pp.947-999.

DOI

A type theory with definitional proof-irrelevance. Gilbert, Gaëtan, PhD Thesis, Ecole nationale supérieure Mines-Télécom Atlantique, December 2019.

Eliminating Dependent Pattern-Matching in Coq. Mangin, Cyprien, Master's Thesis, Université Paris 7 Denis Diderot, August 2015.

Equations Reloaded: High-Level Dependently-Typed Programming and Proving in Coq. Matthieu Sozeau & Cyprien Mangin PACMPL 3 (ICFP), August 2019, pp.86-115.

DOI

Ensembles nominaux dans Coq/SSreflect. Lewertowski, Gabriel, Master's Thesis, Univeristé Paris Diderot Paris 7, September 2015.

The Definitional Side of the Forcing in LICS '16. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau. , 2016, pp.367-376.

DOI

Towards a Proof-Irrelevant Calculus of Inductive Constructions. Haselwarter, Philipp, Master's Thesis, Université Paris 7, September 2014.

Towards an efficient and formally-verified convertibility checker. Nathanaëlle Courant, PhD Thesis, University of Paris, September 2024.

Foreign Function Verification Through Metaprogramming. Joomy Korkut, PhD Thesis, Princeton University, USAPrinceton University, 2024.

Contributions in Programming Languages Theory: Logical Relations and Type Theory. Timany, Amin, PhD Thesis, University of Leuven, May 2018.