A Metatheoretic Analysis of Subtype Universes

Research output: Chapter in Book/Report/Conference proceedingChapter


Subtype universes were initially introduced as an expressive mechanisation of bounded quantification extending a modern type theory. In this paper, we consider a dependent type theory equipped with coercive subtyping and a generalised, more expressive model of subtype universes. We prove results regarding the metatheoretic properties of subtype universes, such as consistency and strong normalisation. We analyse the causes of undecidability in bounded quantification, and we discuss how coherency impacts the metatheoretic properties of theories implementing bounded quantification. We discuss the effects of certain natural choices of subtyping inference rules on the expressiveness of a type theory. We describe applications in natural language semantics, programming languages, and mathematics formalisation.
Original languageEnglish
Title of host publicationLeibniz International Proceedings in Informatics
PublisherSchloss Dagstuhl –Leibniz Center for Informatics
Publication statusSubmitted - 10 Dec 2022

Cite this