Coq for HoTT. Matthieu Sozeau, Invited talk at the International Conference on Mathematical Software in Berlin, Germany, July 14th 2016.
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 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.
- July: at ICMS'16, gave a talk on Coq for HoTT 
- June: at the DeepSpec kickoff meeting in Princeton, NJ, gave a talk on Coq 8.6  and enjoyed a lot of Coq-related talks!
- May: at the second Coq implementors workshop in Nice, gave a talk on Universes  for ML hackers.
- April: our paper  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 
- January: Gave a talk  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  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 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.
Coq 8.5 at work. Maxime Dénès, Matthieu Sozeau, Talk given at the second CoqPL Workshop, St Petersburg, FL, January 2016.
A Unification Algorithm for Coq featuring Universe Polymorphism and Overloading. Matthieu Sozeau, Talk given at ICFP'15, Vancouver, Canada, September 2015.
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.