Universe Polymorphism and Inference in Coq. Matthieu Sozeau, Talk given at TYPES'13, Toulouse, France, April 25th 2013.
Commits are worth a thousand words on my github.
I'll be at ITP-3.
- Apr'13: gave a talk at TYPES'13 on universe polymorphism. 
- Mar'13: gave a seminar on univalence for free  at the Types and Realizability working group.
- Feb'13: gave two lectures at the MPRI, on typeclasses and dependently-typed programming.
- Feb'13: together with Nicolas Tabareau, we wrote an article on univalence and 2-groupoids, submitted .
- Feb '13: at the JFLA'13 in Aussois.
- Sep-Dec '12: at the IAS in Princeton, NJ for the special year on Homotopy type theory. Working specifically on universe polymorphism.
- October'12: gave a lecture at UPenn on type classes  with a nice exercise.
- July'12: at LICS in Croatia with N. Tabareau and G. Jaber for our paper on Forcing in Type Theory .
Univalence for free. Matthieu Sozeau, Talk given at the Types and Realizability Working Group, Paris, 2013.
Coq with Classes. Matthieu Sozeau, Lecture at the "Advanced Martial Arts in Coq" course at University of Pennsylvania, October 2012.