A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading. Matthieu Sozeau, Talk given at ICFP'15, Vancouver, Canada, September 2015.
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.
- September 1st: Gave a talk  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  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  on Coq for proving functional programs at the "École de Printemps d'Informatique Théorique" in Fréjus.
- May 8th: Paper on Equations  and Predicative System F, joint work with Cyprien Mangin accepted at LFMTP'15.
- May: Paper  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  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 .
- January: at POPL'15 in Mumbai, for the first CoqPL workshop, we released Coq 8.5 beta .
- 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 , at ITP on universe polymorphism  and at the Coq workshop on rewriting strategies  and Coq 8.5 .
- May'14: I gave a seminar at the XIX AIM in Paris on universe polymorphism .
- Apr'14: Gave a seminar at the Deducteam HoTT working group on an Internalization of the Groupoid Model of Type Theory .
- Apr'14: Universe Polymorphism in Coq  to appear at ITP'14.
- Feb'14: Draft paper on an Internalization of the Groupoid Model of Type Theory .
- 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  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, Mumbai, India, January 2015.
Towards A Better Behaved Unification Algorithm for Coq. Matthieu Sozeau, Talk given at the UNIF workshop, Vienna, Austria, July 2014.
Proof-relevant rewriting strategies. Matthieu Sozeau, Talk given at the Sixth Coq Workshop, Vienna, Austria, July 2014.
Coq 8.5: What's New, What's Next?. Matthieu Sozeau, Talk given at the Sixth Coq Workshop, Vienna, Austria, July 2014.
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. Vienna, Austria, 2014 - To appear.
Towards an Internalization of the Groupoid Model of Type Theory. Sozeau, Matthieu & Tabareau, Nicolas, Unpublished, February 2014 - Under revision.