Universe Polymorphism and Inference in Coq. Matthieu Sozeau, Talk given at the Institute for Advanced Study, Princeton, NJ, December 5th 2012.
Universe Polymorphism and Inference in Coq
While visiting the IAS for the special year on homotopy type theory, I've been working on an implementation of universe polymorphism and inference in Coq that should sove many of the current problems with the lack of polymorphism in the current system. The github is here and I've given a talk  about it.