*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.

News

You are on Matthieu Sozeau's website, that's me on the right.
I'm a researcher at Inria in the Gallinette team
in Nantes, and the current coordinator of
the Coq project. Commits are worth a thousand words on my github.

### What's next

- I am part of the ICFP'24 Program Committee, which will take place in Milano, Italy. Consider submitting!

### Timeline/Log

#### 2024

- January: I gave an invited talk [1] [2] at JFLA'24 on MetaCoq and our progress on certified extraction to C and OCaml.
- January: Coq 8.19 has been released.
- January: I gave the Coq Developers Session [3] talk at CoqPL'24.
- January: I was part of the WITS 2024 program committee.
- January: The MetaCoq team gave a tutorial at POPL'24.

#### 2023

- November: Together with Yannick Forster and Nicolas Tabareau, we have developed a certified compilation chain from Coq to OCaml/Malfunction and submitted [4] an article on it.
- September: Coq 8.18 has been released.
- July: Antoine Allioux succesfully defended his thesis [5].
- July: Giving a lecture on MetaCoq and CertiCoq at the 2023 Summer School on Proof Theory and its Applications
- June: Pierre-Marie Pédrot presented our joint work on sort polymorphism [6] at TYPES 2023 in Valencia.
- April: Together with Yannick Forster, Jakob Botsh Nielsen, Meven Lennon-Bertrand, Nicolas Tabareau and Théo Winterhalter we submitted [7] a journal article on the whole MetaCoq project (version 1.2), now with soundness and completeness of the type-checking and conversion implementations, optimized environment handling and a completely verified erasure pipeline.
- April: MetaCoq version 1.2 [8] has been released.
- January: Coq 8.17+rc1 was released.
- January-March: teaching MPRI 2-7-2, a lecture on proof assistants.

#### 2022

- October: CertiCoq 0.9 beta was released, the first ever verified compiler from Coq to assembly, starting from MetaCoq erased terms and going through CompCert.
- October: Equations 1.3 for Coq 8.17 was released [9], fixing performance issues and bugs.
- October: MetaCoq 1.1.1 was released [10], providing a fully certified checker for Coq and verified erasure.
- September: Yannick Forster presented our joint work on extraction to OCaml from Coq [11]
- June: I co-organized the TYPES 2022 Conference in Nantes with Nicolas Tabareau.
- January-March: teaching MPRI 2-7-2, a lecture on proof assistants.
- January: attended POPL 2022, CoqPL where I gave the traditional Coq Development News [12] and the WITS workshop where I talked about case representation in Coq and MetaCoq [13].
- January: Coq 8.15 was released [14].

#### 2021

- November: Equations 1.3 was released [15].
- October: Coq 8.14 was released [16].
- October: I gave an invited talk at the HoTTest seminar on the MetaCoq Project [17].
- July: I gave an invited talk [18] at the LFMTP'21 workshop affiliated with CADE 28 on the MetaCoq project. The accompanying paper [19] describes the current state of the project.
- July: Together with Kenji Maillard, Nicolas Margulies, Nicolas Tabareau and Eric Tanter, we have submitted a new article on the Multiverse [20], a system to gain logical modularity in proof assistants.
- June: I attended the LICS/ITP 2021 conference and gave a talk [21] on Coq at the Coq Workshop 2021.
- June: I attended the TYPES 2021 conference, and became a new member of the Steering Comittee of TYPES.
- April: I co-organized with Nicolas Tabareau the EPIT 2020 Spring School on Homotopy Type Theory, online.
- March: I was a PC member of the ITP 2021 conference.
- February: Together with Théo Winterhalter, we gave a talk on Coq Coq Correct! [22] online at the Cambium Team seminar, Inria Paris.
- January: Together with Antoine Allioux and Eric Finster, we submitted an article [23] showing that extending univalent/homotopy type theory with polynomial monads suffices to internally build the equivalence between infinity-groupoids and types, check it out! It will be presented at LICS 2021.
- I attended POPL 2021 (online) and gave a talk on Coq Development [24] at CoqPL'21.

#### 2020

- Our article [25] on mixing univalence and parametricity was accepted at the JACM, joint work with Nicolas Tabareau and Éric Tanter.
- Taught Proof Assistants at the MPRI.
- I was part of the POPL'21 program committee.
- I moved to the Gallinette team in Nantes, a team of Inria Bretagne-Atlantique.
- I gave a Tutorial on Equations at CoqPL'20.
- Taught Coq + Equations at the Coq Andes Summer School (CASS) 2020 in Santuario del Río, San José del Maipo, Chile, Jan 6-10 2020.

#### 2019

- Visited Bas Spitters' group in Aarhus and gave a guest lecture on Equations for dependently-typed programming in Coq.
- October: paper "Coq Coq Correct!" [26], on the verification of typechecking and erasure for Coq in Coq was accepted at POPL'20.
- September-December: teaching MPRI 2-7-2 lecture on proof assistatnts.
- September: Yannick Forster presented Coq Coq Codet! [27] at the 10th Coq Workshop colocated with ITP19.
- August: presented Equations Reloaded [28] at ICFP 2019.
- August: talked about Equations for HoTT [29] at the Homotopy Type Theory 2019 conference.
- June-July: Visiting Benjamin Pierce's group at the University of Pennsylvania
- June: Equations Reloaded [30] was accepted for publication at ICFP'19.
- May: Coq 8.10beta1 (with SProp!) and Equations 1.2 were released.
- May: I gave a seminar on MetaCoq and CertiCoq [31] at Nomadic Labs.
- April: submitted an extended version of our ITP'18 paper on The MetaCoq Project [32] to JAR.
- February: I gave an introductory lecture on certified programming and proof assistants [33] for the Master 1 of Computer Science at Paris 7.
- January: I gave a seminar on Definitional Proof-Irrelevance without K [34] at the Deducteam seminar.
- January: Equations 1.2beta was released.
- January: Coq 8.9.0 was released.
- January: Attended POPL'19.

#### 2018

- December: I gave a seminar on programming with Coq [35] attached to Xavier Leroy's lectures on Curry-Howard Today at the Collège de France.
- November: I gave a talk on our universe of strict propositions [36] and Eric Finster gave one on higher universal algebra in type theory at the PPS days.
- October: I gave a talk on the MetaCoq Project [37] at the VALS seminar.
- October: Definitional Proof-Irrelevance without K [38] has been accepted at POPL'19. We present a version of definitionally strict propositions compatible with univalent models. Soon to be found in Coq!
- September-November: MPRI 2.7.2 lecture on proof assistants.
- September: we got the distinguished paper award for our paper "Equivalences for Free!" [39] at ICFP'18.
- September: I am part of the LSFA 2018 program comittee, which will happen in Fortaleza, Brazil in September 2018.
- September: I am part of the TyDe 2018 program comittee colocated with ICFP 2018 in St. Louis, MI.
- August: introductory lecture on Dependent Type Theory at the EUTYPES summer school 2018.
- July: I was part of the ITP 2018 program comittee, and co-organizing the Coq Workshop at FLoC 2018.
- June: I gave an invited talk [40] at the TYPES 2018 conference in Braga, Portugal, June 18-21.
- April: I was an examiner of Amin Timany's PhD, who defended successfully his thesis in KU Leuven, Belgium.
- April 26th: I gave a guest lecture [41] on dependent pattern-matching and Equations at the University of Saarland.
- April 10-11th: participated in the pi.r2 days in Fontainebleau and gave a general talk on Coq as "An Environment for Programming with Dependent Types, take II". Our team is a quite interesting mix!
- April: our paper on Cumulative Inductive Types [42] was accepted at FSCD'18.
- April: our paper on Certified Meta-Programming with Typed Template Coq [43] was accepted at ITP'18.
- March: submitted papers on Equations, an effective ETT to ITT translation [44] and Equivalences for Free! to ICFP.
- January: I attended the EUTypes meeting in Nijmegen where I gave a short talk on handling of recursion in Equations [45].
- January: I attended POPL 2018, PEPM, CPP and CoqPL as well. Giving a presentation + poster at PEPM 2018 on Equations [46], a talk on Typed Template Coq [47] at CoqPL'18, along with the traditional .

#### 2017

- November: participated to the Géocal-LAC days in Nantes, and gave a talk on cumulative inductives types [48].
- October: Coq 8.7 was released, including cumulative inductive types. With Amin Timany, we proved the consistency [49] of this extension using a set-theoretic model.
- October: released Equations version 1.0beta with a handful of examples, and submitted an article on the new version, joint work with Cyprien Mangin.
- October: new article on deriving Equivalences for free with Nicolas Tabareau and Eric Tanter.
- October: with Amin Timany, we proved the soundness of our extension of Coq with Cumulative Inductive Types.
- September: Théo Winterhalter started his PhD in the CoqHoTT team, co-supervised with Nicolas Tabareau.
- June: branching version 8.7 of Coq, which includes cumulative inductive types and integrates the ssreflect plugin.
- June: gave a lecture at EJCP'17 on Type Theory and Interactive Theorem Proving in Coq [50]
- June: at the 3rd Coq's Implementors Workshop in Carnac, Britany.
- May: at TYPES 2017, for our work on cumulative inductive types [51].
- March-April: working on Cumulative Inductive Types with Amin Timany, adding a cumulativity rule to inductives, simulating template polymorphism.
- January-March: MPRI lecture on proof assistants.
- January: Attended CPP 2017, POPL 2017 and CoqPL'17, and had a blast! Greg and Andrew presented our work on CertiCoq [52] there.

#### 2016

- November: we released Coq version 8.6beta1: A Better, Faster, Stronger Rooster!
- November: our paper [53] on the HoTT library got accepted at CPP 2017!.
- November: our presentation on CertiCoq was accepted at CoqPL'17!
- October: the extended version of our paper on was accepted at JFP.
- August: at the ITP 2016 conference and Coq Workshop 2016 in Nancy, where Hugo Herbelin passed me the Coq development coordinator hat [54].
- July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [55]
- July: at ICMS'16, gave a talk on Coq for HoTT [56]
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [57] and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes [58] for ML hackers.
- April: our paper [59] on a new call-by-name forcing translation in Type Theory got accepted at LICS.
- March: at the Dagstuhl seminar on "Language Based Verification Tools for Functional Programs", giving a short talk on Equations [60]
- January: Gave a talk [61] at the CoqPL workshop on Coq 8.5
- January: (finally!) released Coq 8.5, including my work on universe polymorphism and primitive projections.

#### 2015

- December-March: Coq lecture at MPRI
- September 1st: Gave a talk [62] on our work on unification with Beta Ziliani at ICFP'15.
- August 1st: at the LFMTP'15 workshop, where Cyprien presented our work on Equations and Predicative System F.
- June 27th-July 3rd: Gave a lecture [63] at the HoTT/UF workshop and attending TLCA'15 in Warsaw.
- June 22-26: first successful Coq coding sprint in lovely Nice, followed by the Coq Workshop
- June 1st: ERC CoqHoTT started!
- May 26th: Gave a lecture [64] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [65] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [66] on a new unification algorithm for Coq, joint work with Beta Ziliani, accepted at ICFP'15. The Coq plugin is here.
- April 29th: Gave a seminar [67] at MIT on our new unification algorithm.
- April 22nd: Released Coq 8.5 beta 2.
- March: Submitted a new version of our work with Nicolas on Internalizing Intensional Type Theory [68].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [69].
- December-March 2015: Lecturing on proof assistants at the MPRI.

*MetaCoq: Towards a Certified Kernel and Extraction for Coq*. Matthieu Sozeau, Invited talk at JFLAs 2024, Saint-Jacut-de-la-Mer, France, January 31st 2024.

*Verified Extraction from Coq to OCaml*. Forster, Yannick, Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, 2023 - working paper or preprint.

*Higher Structures in Homotopy Type Theory*. Antoine Allioux, PhD Thesis,

*From Lost to the River: Embracing Sort Proliferation*in

*29th International Conference on Types for Proofs and Programs*. Gaëtan Gilbert, Matthieu Sozeau, Pierre-Marie Pédrot & Nicolas Tabareau. , June 2023, pp.14-17.

*Correct and Complete Type Checking and Certified Erasure for Coq, in Coq*. Sozeau, Matthieu, Forster, Yannick, Lennon-Bertrand, Meven, Nielsen, Jakob Botsch, Tabareau, Nicolas & Winterhalter, Théo, Unpublished, April 2023 - Submitted.

*MetaCoq 1.2 for Coq 8.16, version v1.2-8.16*. Matthieu Sozeau, Danil Annenkov, Jakob Botsch Nielsen, Yannick Forster, Jason Gross, Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau & Théo Winterhalter, April 2023.

*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.

*Extraction to OCaml from Coq: Operational Correctness Verified in Coq*. Yannick Forster, Matthieu Sozeau, Pierre Giraud, Pierre-Marie Pédrot & Nicolas Tabareau

*ML Workshop 2022*, September 2022.

*The Curious Case of Case: correct and efficient case representation in Coq and MetaCoq*. Matthieu Sozeau, Talk given at the WITS Workshop,

*The Coq Proof Assistant, version 8.15*. The Coq Development Team, January 2022.

*Equations, version 1.3*. Matthieu Sozeau, January 2022.

*The Coq Proof Assistant, version 8.14*. The Coq Development Team, October 2021.

*The MetaCoq Project*. Matthieu Sozeau, Talk given at the HoTTest Seminar, online, October 2021.

*Touring the MetaCoq Project*. Matthieu Sozeau, Invited talk at LFMTP'21, July 2021.

*The Multiverse: Logical Modularity for Proof Assistants*. Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau & Eric Tanter, Unpublished, July 2021 - Submitted.

*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.

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

*LICS*, January 2021 - Extended version of the LICS 2021 article.

*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.

*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.

*Equations Reloaded*. Matthieu Sozeau, Talk given at ICFP 2019, August 2019.

*Equations for HoTT*. Matthieu Sozeau, Talk given at the Homotopy Type Theory 2019 Conference, August 2019.

*Equations Reloaded: High-Level Dependently-Typed Programming and Proving in Coq*. Matthieu Sozeau & Cyprien Mangin

*PACMPL*3 (ICFP), August 2019, pp.86-115.

*The MetaCoq Project*. Matthieu Sozeau, Talk given at Nomadic Labs,

*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.

*Programmation certifiée et assistants de preuve*. Matthieu Sozeau, Séminaire Introduction à la Recherche, Université Paris Diderot, February 12th 2019.

*Definitional Proof-Irrelevance without K*. Matthieu Sozeau, Talk given at the Deducteam seminar,

*Programmer avec Coq: filtrage dépendant et récursion*. Matthieu Sozeau, Séminaire au Collège de France,

*A Universe of Strict Propositions in Type Theory*. Matthieu Sozeau, Talk given at the PPS Days, IRIF,

*The MetaCoq Project*. Matthieu Sozeau, Talk given at the VALS Seminar, LRI,

*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*. Tabareau, Nicolas, Tanter, Éric & Sozeau, Matthieu

*Proceedings of the ACM on Programming Languages*, September 2018, pp.1-29.

*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.

*A Gentle Introduction to Equations Or How to Match Regexps with Dependently-Typed Continuations*. Matthieu Sozeau, Lecture notes for a guest lecture given at Saarland University,

*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.

*Eliminating Reflection from Type Theory*. Winterhalter, Théo, Sozeau, Matthieu & Tabareau, Nicolas , October 2018 - Accepted at CPP'19.

*Nested, Well-Founded and Mutual recursion in Equations*. Matthieu Sozeau, Talk given at the EUTypes 2018 Working Meeting,

*Equations: From Clauses to Splittings to Functions*. Cyprien Mangin & Matthieu Sozeau, Talk and Poster at PEPM 2018 - ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation,

*Typed Template Coq*in

*CoqPL'18*. Simon Boulier, Matthieu Sozeau, Nicolas Tabareau & Abhishek Anand.

*Cumulative Inductive Types in Coq*. Matthieu Sozeau, Talk at Géocal-LAC days, Nantes, France, November 14th 2017.

*Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)*. Timany, Amin & Sozeau, Matthieu, Technical Report,

*Introduction to Type Theory and Interactive Theorem Proving in Coq*. Matthieu Sozeau, Lecture notes for a course given at EJCP'17 in Toulouse, June 27th 2017.

*Cumulative Inductive Types in Coq*in

*TYPES 2017 Proceedings*. Amin Timany, Matthieu Sozeau & Bart Jacobs.

*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.

*The HoTT Library: A formalization of homotopy type theory in Coq*. Bauer, A., Gross, J., LeFanu Lumsdaine, P., Shulman, M., Sozeau, M. & Spitters, B.

*ArXiv e-prints*, October 2016 - Accepted at CPP'17.

*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.

*Universe Polymorphism for the OCaml hacker*. Matthieu Sozeau, Talk at the Second Coq Implementors Workshop, Sophia-Antipolis, France, June 2nd 2016.

*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.

*Equations: a function definition toolbox for Coq*. Matthieu Sozeau, Talk at Dagstuhl, March 2016.

*Coq 8.5 at work*. Maxime Dénès, Matthieu Sozeau, Talk given at the second CoqPL Workshop,

*A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading*. Matthieu Sozeau, Talk given at ICFP'15,

*Coq support for HoTT*. Matthieu Sozeau, Invited talk at the HoTT/UF workshop in Warsaw, Poland, June 2015.

*Functional Programming and Proving in Coq*. Matthieu Sozeau, Lecture at the "École de Printemps d'Informatique Théorique 2015" in Fréjus, France, May 2015.

*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 Unification Algorithm for Coq featuring Universe Polymorphism and Overloading*in

*ACM SIGPLAN International Conference on Functional Programming 2015*. Beta Ziliani & Matthieu Sozeau. , 2015.

*A Predictable Unification Algorithm for Coq*. Matthieu Sozeau, Talk given at MIT, Cambridge, MA, April 29th 2015.

*Internalizing Intensional Type Theory*. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2015.

*Coq dev talk*. Matthieu Sozeau, Talk given at the First CoqPL workshop,