2026-08-07T10:04:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13888 2024-03-06T10:52:44Z ddc:004 open_access

Subtype Universes Maclean, Harry Luo, Zhaohui Type theory coercive subtyping subtype universe 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Harry Maclean and Zhaohui Luo 2021 Is Part Of LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2020.9 urn:nbn:de:0030-drops-138880 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.9 eng https://creativecommons.org/licenses/by/4.0/legalcode