Universe Polymorphism and Inference in Coq. Matthieu Sozeau, Talk given at TYPES'13, Toulouse, France, April 25th 2013.
News
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. [1]
- Mar'13: gave a seminar on univalence for free [2] 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 [3].
- 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 [4] with a nice exercise.
- July'12: at LICS in Croatia with N. Tabareau and G. Jaber for our paper on Forcing in Type Theory [5].
Univalence for free. Matthieu Sozeau, Talk given at the Types and Realizability Working Group, Paris, 2013.
Univalence for free. Sozeau, Matthieu and Tabareau, Nicolas, Unpublished, February 2013.
Coq with Classes. Matthieu Sozeau, Lecture at the "Advanced Martial Arts in Coq" course at University of Pennsylvania, October 2012.
Extending Type Theory with Forcing in Proceedings of LICS'12. Jaber, Guilhem and Tabareau, Nicolas and Sozeau, Matthieu. Dubrovnik, Croatie , June 2012.
