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 publication28th International Conference on Types for Proofs and Programs (TYPES 2022)
Subtitle of host publicationLeibniz International Proceedings in Informatics
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl –Leibniz Center for Informatics
Number of pages21
ISBN (Electronic)978-3-95977-285-3
Publication statusAccepted/In press - 28 Jul 2023


  • type theory
  • mathematics
  • logic
  • subtype universes
  • subtyping
  • bounded quantification

Cite this