License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2020.9
URN: urn:nbn:de:0030-drops-138880
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13888/
Maclean, Harry ;
Luo, Zhaohui
Subtype Universes
Abstract
We introduce a new concept called a subtype universe, which is a collection of subtypes of a particular type. Amongst other things, subtype universes can model bounded quantification without undecidability. Subtype universes have applications in programming, formalisation and natural language semantics. Our construction builds on coercive subtyping, a system of subtyping that preserves canonicity. We prove Strong Normalisation, Subject Reduction and Logical Consistency for our system via transfer from its parent system UTT[ℂ]. We discuss the interaction between subtype universes and other sorts of universe and compare our construction to previous work on Power types.
BibTeX - Entry
@InProceedings{maclean_et_al:LIPIcs.TYPES.2020.9,
author = {Maclean, Harry and Luo, Zhaohui},
title = {{Subtype Universes}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-182-5},
ISSN = {1868-8969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13888},
URN = {urn:nbn:de:0030-drops-138880},
doi = {10.4230/LIPIcs.TYPES.2020.9},
annote = {Keywords: Type theory, coercive subtyping, subtype universe}
}
|
Keywords: |
|
Type theory, coercive subtyping, subtype universe |
|
Collection: |
|
26th International Conference on Types for Proofs and Programs (TYPES 2020) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
07.06.2021 |
