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

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 will co-organize the TYPES 2022 Conference in Nantes in June 2022.

### Timeline/Log

#### 2022

- 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 [1] and the WITS workshop where I talked about case representation in Coq and MetaCoq [2].
- January: Coq 8.15 was released [3].

#### 2021

- November: Equations 1.3 was released [4].
- October: Coq 8.14 was released [5].
- October: I gave an invited talk at the HoTTest seminar on the MetaCoq Project [6].
- July: I gave an invited talk [7] at the LFMTP'21 workshop affiliated with CADE 28 on the MetaCoq project. The accompanying paper [8] 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 [9], a system to gain logical modularity in proof assistants.
- June: I attended the LICS/ITP 2021 conference and gave a talk [10] 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! [11] online at the Cambium Team seminar, Inria Paris.
- January: Together with Antoine Allioux and Eric Finster, we submitted an article [12] 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 [13] at CoqPL'21.

#### 2020

- Our article [14] 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!" [15], 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! [16] at the 10th Coq Workshop colocated with ITP19.
- August: presented Equations Reloaded [17] at ICFP 2019.
- August: talked about Equations for HoTT [18] at the Homotopy Type Theory 2019 conference.
- June-July: Visiting Benjamin Pierce's group at the University of Pennsylvania
- June: Equations Reloaded [19] 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 [20] at Nomadic Labs.
- April: submitted an extended version of our ITP'18 paper on The MetaCoq Project [21] to JAR.
- February: I gave an introductory lecture on certified programming and proof assistants [22] for the Master 1 of Computer Science at Paris 7.
- January: I gave a seminar on Definitional Proof-Irrelevance without K [23] 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 [24] 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 [25] 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 [26] at the VALS seminar.
- October: Definitional Proof-Irrelevance without K [27] 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!" [28] 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 [29] 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 [30] 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 [31] was accepted at FSCD'18.
- April: our paper on Certified Meta-Programming with Typed Template Coq [32] was accepted at ITP'18.
- March: submitted papers on Equations, an effective ETT to ITT translation [33] 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 [34].
- January: I attended POPL 2018, PEPM, CPP and CoqPL as well. Giving a presentation + poster at PEPM 2018 on Equations [35], a talk on Typed Template Coq [36] 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 [37].
- October: Coq 8.7 was released, including cumulative inductive types. With Amin Timany, we proved the consistency [38] 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 [39]
- June: at the 3rd Coq's Implementors Workshop in Carnac, Britany.
- May: at TYPES 2017, for our work on cumulative inductive types [40].
- 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 [41] there.

#### 2016

- November: we released Coq version 8.6beta1: A Better, Faster, Stronger Rooster!
- November: our paper [42] 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 [43].
- July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [44]
- July: at ICMS'16, gave a talk on Coq for HoTT [45]
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [46] and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes [47] for ML hackers.
- April: our paper [48] 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 [49]
- January: Gave a talk [50] 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 [51] 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 [52] 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 [53] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [54] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [55] 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 [56] 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 [57].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [58].
- December-March 2015: Lecturing on proof assistants at the MPRI.

*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 ∞-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,