The Multiverse: Logical Modularity for Proof Assistants. Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau & Eric Tanter, Unpublished, July 2021 - Submitted.
Curriculum Vitæ
Pdf version.
Matthieu Sozeau
Adress:
8 rue Jean Poulain
44300 Nantes
France
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 Coq development team since 2016 and major contributor to Coq since 2005.
- Lead developer of the Coq Equations plugin and the MetaCoq 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 ofChristine 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.
Drafts
Books
- Homotopy Type Theory: Univalent Foundations for Mathematics. The Univalent Foundations Program.
Journals
- The Marriage of Univalence and Parametricity. Tabareau, Nicolas, Tanter, Éric & Sozeau, Matthieu J. ACM 68 (1), January 2021.
- 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.
- 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.
- Equations Reloaded: High-Level Dependently-Typed Programming and Proving in Coq. Matthieu Sozeau & Cyprien Mangin PACMPL 3 (ICFP), August 2019, pp.86-115.
- 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.
- Equivalences for free: univalent parametricity for effective transport. Nicolas Tabareau, Éric Tanter & Matthieu Sozeau PACMPL 2 (ICFP), 2018, pp.92:1-92:29.
- 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.
- 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.
- 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 - Extended version of the LICS 2021 article.
- 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.
- Cumulative Inductive Types In Coq in FSCD. Amin Timany & Matthieu Sozeau. , July 2018, pp.29:1-29:16.
- Towards Certified Meta-Programming with Typed Template-Coq in ITP 2018. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau & Nicolas Tabareau.
- 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.
- 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.
- 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.
- Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem, Tabareau, Nicolas & Sozeau, Matthieu.
- Equations: A Dependent Pattern-Matching Compiler in First International Conference on Interactive Theorem Proving. Matthieu Sozeau.
- (18/40)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©
- (26/103)Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau.©
- (17/29)Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of©
International Workshops
- Touring the MetaCoq Project in LFMTP 2021. Matthieu Sozeau.
- 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,
- Typed Template Coq in CoqPL'18. Simon Boulier, Matthieu Sozeau, Nicolas Tabareau & Abhishek Anand.
- 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.
- 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
- A New Look at Generalized Rewriting in Type Theory. Matthieu Sozeau 1st Coq Workshop proceedings, August 2009.
National Conferences
- Classes de types de première classe in Journées Nationales du GDR GPL. Matthieu Sozeau & Nicolas Oury.
Theses
- Un environnement pour la programmation avec types dépendants. Matthieu Sozeau, PhD Thesis,
- Coercion par prédicats en Coq. Matthieu Sozeau, Master's Thesis,
Research Reports
- Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Timany, Amin & Sozeau, Matthieu, Technical Report,
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.
- 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.
- Equations, version 1.3. Matthieu Sozeau, January 2022.
- Equations, version 1.0. Matthieu Sozeau & Cyprien Mangin, December 2017.
- The Coq Proof Assistant, version 8.16. The Coq Development Team, September 2022.
- The Coq Proof Assistant, version 8.15. The Coq Development Team, January 2022.
- The Coq Proof Assistant, version 8.14. The Coq Development Team, October 2021.
- The Coq Proof Assistant, version 8.13. The Coq Development Team, January 2021.
- The Coq Proof Assistant, version 8.12. The Coq Development Team, July 2020.
- The Coq Proof Assistant, version 8.11. The Coq Development Team, January 2020.
- The Coq Proof Assistant, version 8.10. The Coq Development Team, October 2019.
- The Coq Proof Assistant, version 8.9. The Coq Development Team, January 2019.
- The Coq Proof Assistant, version 8.8.0. The Coq Development Team, Apr 2018.
- The Coq Proof Assistant, version 8.7.1. The Coq Development Team, December 2017.
- 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.
- `User defined equalities and relations' in Coq Reference Manual. Matthieu Sozeau.
- `Program' in Coq Reference Manual. Matthieu Sozeau.
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,
- 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.
- Coq Development in CoqPL'20. Maxime Dénès & Matthieu Sozeau.
- Coq Development in CoqPL'19. Maxime Dénès & Matthieu Sozeau.
- 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.
- Coq Development in CoqPL'17. Matthieu Sozeau.
- 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,
- 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,
- An Environment for Proving and Programming. Matthieu Sozeau, LIFO Seminar,
- An Environment for Programming with Dependent Types. Matthieu Sozeau, ICIS Seminar,
- First-Class Type Classes. Matthieu Sozeau, Talk given at the Gallium seminar,
- Program-ing in Coq. Matthieu Sozeau, Talk given at the Foundations of Programming seminar,
- Program-ing in Coq. Matthieu Sozeau, Talk given at Harvard,
- Program-ing in Coq. Matthieu Sozeau, Talk given at Portland State University,
- Program-ing in Coq. Matthieu Sozeau, Talk given at the Gallium seminar,
Hobbies
- Music: Guitar, Bass and Drums.
- Dance: Forró and Lindy-Hop
