1 Search Results for "Maclean, Harry"

Document
DOI: 10.4230/LIPIcs.TYPES.2020.9
Subtype Universes

Authors: Harry Maclean and Zhaohui Luo

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

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.
Cite as

Harry Maclean and Zhaohui Luo. Subtype Universes. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.9},
  URN =		{urn:nbn:de:0030-drops-138880},
  doi =		{10.4230/LIPIcs.TYPES.2020.9},
  annote =	{Keywords: Type theory, coercive subtyping, subtype universe}
}
  • Refine by Author
  • 1 Luo, Zhaohui
  • 1 Maclean, Harry

  • Refine by Classification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Type theory
  • 1 coercive subtyping
  • 1 subtype universe

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact