Larry Diehl, Tim Sheard. Leveling up dependent types: generic programming over a predicative hierarchy of universes. In Stephanie Weirich, editor, Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming, DTP@ICFP 2013, Boston, Massachusetts, USA, September 24, 2013. pages 49-60, ACM, 2013. [doi]
Abstract is missing.