A Metatheoretic Analysis of Subtype Universes

Felix Bradley; Zhaohui Luo

doi:10.4230/LIPIcs.TYPES.2022.9

A Metatheoretic Analysis of Subtype Universes

Research output: Chapter in Book/Report/Conference proceeding › Chapter

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	https://doi.org/10.4230/LIPIcs.TYPES.2022.9
Publication status	Accepted/In press - 28 Jul 2023

Keywords

type theory
mathematics
logic
subtype universes
subtyping
bounded quantification

Access to Document

10.4230/LIPIcs.TYPES.2022.9Licence: CC BY

Subtype Universes
Bradley, F. (PI)
19/04/22 → 10/12/22
Project: Research

On the Metatheory of Subtype Universes (TYPES23)
Bradley, F. (Speaker)
12 Jun 2023 → 15 Jun 2023
Activity: Talk or presentation › Oral presentation

File
On the Metatheory of Subtype Universes (WG6)
Bradley, F. (Speaker)
24 Apr 2023
Activity: Talk or presentation › Oral presentation

File

Cite this

@inbook{268e628a6ae045c89041f4f7daa4b9e8,

title = "A Metatheoretic Analysis of Subtype Universes",

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.",

keywords = "type theory, mathematics, logic, subtype universes, subtyping, bounded quantification",

author = "Felix Bradley and Zhaohui Luo",

year = "2023",

month = jul,

day = "28",

doi = "10.4230/LIPIcs.TYPES.2022.9",

language = "English",

volume = "269",

booktitle = "28th International Conference on Types for Proofs and Programs (TYPES 2022)",

publisher = "Schloss Dagstuhl –Leibniz Center for Informatics",

}

TY - CHAP

T1 - A Metatheoretic Analysis of Subtype Universes

AU - Bradley, Felix

AU - Luo, Zhaohui

PY - 2023/7/28

Y1 - 2023/7/28

N2 - 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.

AB - 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.

KW - type theory

KW - mathematics

KW - logic

KW - subtype universes

KW - subtyping

KW - bounded quantification

U2 - 10.4230/LIPIcs.TYPES.2022.9

DO - 10.4230/LIPIcs.TYPES.2022.9

M3 - Chapter

VL - 269

BT - 28th International Conference on Types for Proofs and Programs (TYPES 2022)

PB - Schloss Dagstuhl –Leibniz Center for Informatics

CY - Dagstuhl, Germany

ER -

A Metatheoretic Analysis of Subtype Universes

Abstract

Keywords

Access to Document

Projects

Subtype Universes

Activities

On the Metatheory of Subtype Universes (TYPES23)

On the Metatheory of Subtype Universes (WG6)

Cite this