*Cumulative Inductive Types in Coq*in

*FSCD*. Amin Timany & Matthieu Sozeau.

News

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

- I'm an examiner of Amin Timany's PhD, which he will defend in April 2018 in KU Leuven, Belgium.
- I'm an invited speaker at the TYPES 2018 conference in Braga, Portugal, June 18-21.
- 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!

- April: our paper on Cumulative Inductive Types [1] was accepted at FSCD'18.
- April: our paper on Certified Meta-Programming with Typed Template Coq [2] was accepted at ITP'18.
- March: submitted papers on Equations Reloaded [3], an effective ETT to ITT translation [4] and Equivalences for Free! [5] to ICFP.
- January: I attended the EUTypes meeting in Nijmegen where I gave a short talk on handling of recursion in Equations [6].
- January: I attended POPL 2018, PEPM, CPP and CoqPL as well. Giving a presentation + poster at PEPM 2018 on Equations [7], a talk on Typed Template Coq [8] at CoqPL'18, along with the traditional Coq developer session [9].

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

- November: we released Coq version 8.6beta1: A Better, Faster, Stronger Rooster!
- November: our paper [18] 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 [19].
- July: at the Categorical Logic & Univalent Foundations workshop in Leeds, talking about forcing [20]
- July: at ICMS'16, gave a talk on Coq for HoTT [21]
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [22] and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes [23] for ML hackers.
- April: our paper [24] 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 [25]
- January: Gave a talk [26] at the CoqPL workshop on Coq 8.5
- January: (finally!) released Coq 8.5, including my work on universe polymorphism and primitive projections.

- December-March: Coq lecture at MPRI
- September 1st: Gave a talk [27] 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 [28] 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 [29] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [30] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [31] 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 [32] 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 [33].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [34].
- December-March 2015: Lecturing on proof assistants at the MPRI.

- 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 [35], at ITP on universe polymorphism [36] and at the Coq workshop on rewriting strategies [37] and Coq 8.5 [38].
- May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [39].
- Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [40].
- Apr'14: Universe Polymorphism in Coq [41] to appear at ITP'14.
- Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [42].
- 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 [43] 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.

Copyright © 2006-2015 Matthieu Sozeau