*Coq for HoTT*. Matthieu Sozeau, Invited talk at the International Conference on Mathematical Software in Berlin, Germany, July 14th 2016.

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'll be at ICMS in Berlin and at the Categorical Logic and
Univalent foundations workshop in Leeds in July.

### What I'm up to now

Currently, I'm playing with Induction-Induction and
Induction-Recursion in Coq with
Pierre-Évariste Dagand and CoqHoTT members,
generalizing
generalized rewriting with Théo Zimmerman based on Jérémie
Koenig's logical
relation library
and a
backtracking eauto unifying typeclass resolution and

eauto

.
With C. Mangin we're looking at making Equations
more expressive, fast and robust.
### Timeline/Log

#### 2016

- July: at ICMS'16, gave a talk on Coq for HoTT [1]
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6 [2] and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes [3] for ML hackers.
- April: our paper [4] 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 [5]
- January: Gave a talk [6] 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 [7] 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 [8] 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 [9] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [10] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [11] 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 [12] 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 [13].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [14].
- 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 [15], at ITP on universe polymorphism [16] and at the Coq workshop on rewriting strategies [17] and Coq 8.5 [18].
- May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [19].
- Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [20].
- Apr'14: Universe Polymorphism in Coq [21] to appear at ITP'14.
- Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [22].
- 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 [23] 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.

*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 Forcing*in

*LICS*. Guilhem Jaber, Gabriel Lewertowsky, Pierre-Marie Pédrot, Matthieu Sozeau & Nicolas Tabareau. , April 2016.

*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*. Mangin, Cyprien & Sozeau, Matthieu, Unpublished, May 2015 - LFMTP'15.

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

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