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

News

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

I'll be at POPL'16 and CoqPL in St Petersburg, FL.

### 2015

- September 1st: Gave a talk [1] 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 [2] 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 [3] on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations [4] and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper [5] 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 [6] 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 [7].
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta [8].
- 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 [9], at ITP on universe polymorphism [10] and at the Coq workshop on rewriting strategies [11] and Coq 8.5 [12].
- May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism [13].
- Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory [14].
- Apr'14: Universe Polymorphism in Coq [15] to appear at ITP'14.
- Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory [16].
- 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 [17] 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 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.