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

News

You are on Matthieu Sozeau's website, that's me on the right.
Commits are worth a thousand words on my github.

### What's next

- I will be coorganizing the EPIT 2020 Spring School with Nicolas Tabareau on Homotopy Type Theory, at Oléron, May 25-29 2020
- I'm an examiner of Amin Timany's PhD, which he will defend in April 2018 in KU Leuven, Belgium.
- I will give an introductory lecture on Dependent Type Theory at the EUTYPES summer school 2018.
- I'm part of the ITP 2018 program comittee, and co-organizing the Coq Workshop, consider submitting and coming to FLoC 2018!
- I'm part of the LSFA 2018 program comittee, which will happen in Fortaleza, Brazil in September 2018.
- I'm part of the TyDe 2018 program comittee colocated with ICFP 2018 in St. Louis, MI, consider submitting your best type-driven developments there!

### Timeline/Log

#### 2018

- June: I gave an invited talk [1] at the TYPES 2018 conference in Braga, Portugal, June 18-21.
- May: our paper "Equivalences for Free!" [28] on mixing univalence and parametricity with Nicolas Tabareau and Eric Tanter was accepted at ICFP'18.
- April 26th: I gave a guest lecture [3] 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 [4] was accepted at FSCD'18.
- April: our paper on Certified Meta-Programming with Typed Template Coq [5] was accepted at ITP'18.
- March: submitted papers on Equations Reloaded [6], an effective ETT to ITT translation [7] and Equivalences for Free! [28] to ICFP.
- January: I attended the EUTypes meeting in Nijmegen where I gave a short talk on handling of recursion in Equations [9].
- January: I attended POPL 2018, PEPM, CPP and CoqPL as well. Giving a presentation + poster at PEPM 2018 on Equations [10], a talk on Typed Template Coq [11] at CoqPL'18, along with the traditional Coq developer session [12].

#### 2017

- November: participated to the Géocal-LAC days in Nantes, and gave a talk on cumulative inductives types [13].
- October: Coq 8.7 was released, including cumulative inductive types. With Amin Timany, we proved the consistency [14] 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 [15], joint work with Cyprien Mangin.
- October: new article on deriving Equivalences for Free [16] with Nicolas Tabareau and Eric Tanter.
- October: with Amin Timany, we proved the soundness of our extension of Coq with Cumulative Inductive Types [17].
- 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 [18]
- June: at the 3rd Coq's Implementors Workshop in Carnac, Britany.
- May: at TYPES 2017, for our work on cumulative inductive types [19].
- 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 [20] there.

#### 2016

- November: we released Coq version 8.6beta1: A Better, Faster, Stronger Rooster!
- November: our paper [21] 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 [22].
- July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [23]
- July: at ICMS'16, gave a talk on Coq for HoTT [24]
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [25] and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes [26] for ML hackers.
- April: our paper [27] 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 [28]
- January: Gave a talk [29] 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 [30] 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 [31] 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 [32] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [33] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [34] 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 [35] 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 [36].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [37].
- December-March 2015: Lecturing on proof assistants at the MPRI.

#### 2014

- November: ERC Starting Grant CoqHoTT got granted! Led by Nicolas Tabareau, it will explore the use of Coq for Homotopy Type Theory.
- October: teaching formal methods of verification at Paris 7.
- September'14: at ICFP'14 as part of the SRC and the Heidelberg Laureate Forum.
- July'14: during the Vienna Summer of Logic, I gave talks at the UNIF workshop on unification in Coq [38], at ITP on universe polymorphism [39] and at the Coq workshop on rewriting strategies [40] and Coq 8.5 [41].
- May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [42].
- Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [43].
- Apr'14: Universe Polymorphism in Coq [44] to appear at ITP'14.
- Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [45].
- Jan-Feb'14: Lecturing on proof assistants at the MPRI. My page about the lecture with links to slides and solutions to the exercises.
- Jan'14: Gave a talk [46] with Gérard Huet at POPL'14 for the reception of the 2013 ACM SIGPLAN Software Systems Award by the Coq team.
- Jan'14: Thanks developers and users for a (first, secret,) great Coq Users Meeting at POPL'14, the minutes are available. Looking forward to next year's meeting in Bombay!
- Jan'14: At JFLA'14 and the SMC week on Recent developments in Type Theory in Lyon.

*Equivalences for Free!*. Nicolas Tabareau, Éric Tanter & Matthieu Sozeau, Unpublished, March 2018 - Submitted to ICFP.

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

*Towards Certified Meta Programming with Typed Template-Coq*in

*ITP*. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau & Nicolas Tabareau. , January 2018 - Accepted.

*Equations Reloaded*. Cyprien Mangin & Matthieu Sozeau, Unpublished, March 2018 - Submitted to ICFP.

*Eliminating Reflection from Type Theory*. Winterhalter, Théo, Tabareau, Nicolas & Sozeau, Matthieu , March 2018 - Submitted to ICFP.

*Equivalences for Free!*. Nicolas Tabareau, Éric Tanter & Matthieu Sozeau, Unpublished, March 2018 - Submitted to ICFP.

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

*Coq dev talk*in

*CoqPL'18*. Matthieu Sozeau, Maxime Dénès & Yves Bertot.

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

*Equations Reloaded*. Mangin, Cyprien & Sozeau, Matthieu, Unpublished, October 2017 - Submitted.

*Equivalences for Free!*. Tabareau, Nicolas, Tanter, Eric & Sozeau, Matthieu, Unpublished, October 2017 - Submitted.

*Cumulative Inductive Types in Coq*. Timany, Amin & Sozeau, Matthieu, Unpublished, October 2017 - Submitted.

*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

*Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016*. 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,

*Towards A Better Behaved Unification Algorithm for Coq*. Matthieu Sozeau, Talk given at the UNIF workshop,

*Universe Polymorphism in Coq*. Matthieu Sozeau, Talk at ITP'14, Vienna, Austria, July 16th 2014.

*Proof-relevant rewriting strategies*. Matthieu Sozeau, Talk given at the Sixth Coq Workshop,

*Coq 8.5: What's New, What's Next?*. Matthieu Sozeau, Talk given at the Sixth Coq Workshop,

*Universe Polymorphism: Subtyping and Unification*. Matthieu Sozeau, Invited talk at the Agda Implementers Meeting, Paris, France, May 27th 2014.

*Towards an Internalization of the Groupoid Model of Type Theory*. Sozeau, Matthieu & Tabareau, Nicolas, Misc, April 2014.

*Universe Polymorphism in Coq*in

*ITP'14*. Matthieu Sozeau & Nicolas Tabareau.

*Towards an Internalization of the Groupoid Model of Type Theory*. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Under revision.

*Coq - Recent History*. Matthieu Sozeau, SIGPLAN Programming Language Software Award 2013 talk, at POPL'14, San Diego, January 23rd 2014.