Projects per year
Abstract
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 language | English |
|---|---|
| Title of host publication | 28th International Conference on Types for Proofs and Programs (TYPES 2022) |
| Subtitle of host publication | Leibniz International Proceedings in Informatics |
| Place of Publication | Dagstuhl, Germany |
| Publisher | Schloss Dagstuhl –Leibniz Center for Informatics |
| Number of pages | 21 |
| Volume | 269 |
| ISBN (Electronic) | 978-3-95977-285-3 |
| DOIs | |
| Publication status | Accepted/In press - 28 Jul 2023 |
Keywords
- type theory
- mathematics
- logic
- subtype universes
- subtyping
- bounded quantification
Projects
- 1 Finished
Activities
- 2 Oral presentation
-
On the Metatheory of Subtype Universes (TYPES23)
Felix Bradley (Speaker)
12 Jun 2023 → 15 Jun 2023Activity: Talk or presentation › Oral presentation
File -
On the Metatheory of Subtype Universes (WG6)
Felix Bradley (Speaker)
24 Apr 2023Activity: Talk or presentation › Oral presentation
File