License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.27
URN: urn:nbn:de:0030-drops-54904
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5490/
Go to the corresponding LIPIcs Volume Portal

Assaf, Ali

A Calculus of Constructions with Explicit Subtyping

pdf-format:
4.pdf (0.5 MB)

Abstract

The calculus of constructions can be extended with an infinite hierarchy of universes and cumulative subtyping. Subtyping is usually left implicit in the typing rules. We present an alternative version of the calculus of constructions where subtyping is explicit. We avoid problems related to coercions and dependent types by using the Tarski style of universes and by adding equations to reflect equality.

BibTeX - Entry

@InProceedings{assaf:LIPIcs:2015:5490,
  author =	{Ali Assaf},
  title =	{{A Calculus of Constructions with Explicit Subtyping}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{27--46},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5490},
  URN =		{urn:nbn:de:0030-drops-54904},
  doi =		{10.4230/LIPIcs.TYPES.2014.27},
  annote =	{Keywords: type theory, calculus of constructions, universes, cumulativity, subtyping}
}

Keywords: type theory, calculus of constructions, universes, cumulativity, subtyping
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI