Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang. CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada. pages 143-151, IEEE Computer Society, 2011. [doi]
Abstract is missing.