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.2013.169
URN: urn:nbn:de:0030-drops-46318
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4631/
Go to the corresponding LIPIcs Volume Portal

Herbelin, Hugo ; Spiwack, Arnaud

The Rooster and the Syntactic Bracket

pdf-format:
10.pdf (0.4 MB)

Abstract

We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions toward from smaller sorts to bigger sorts via explicit type construction, as well as impredicative sorts. Type families in impredicative sorts are constructed with a bracketing operation. The necessary restrictions of pattern-matching from impredicative sorts to types are confined to the bracketing construct. This type theory gives an alternative presentation to the calculus of inductive constructions on which the Coq proof assistant is an implementation.

BibTeX - Entry

@InProceedings{herbelin_et_al:LIPIcs:2014:4631,
  author =	{Hugo Herbelin and Arnaud Spiwack},
  title =	{{The Rooster and the Syntactic Bracket}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{169--187},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Ralph Matthes and Aleksy Schubert},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4631},
  URN =		{urn:nbn:de:0030-drops-46318},
  doi =		{10.4230/LIPIcs.TYPES.2013.169},
  annote =	{Keywords: Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families}
}

Keywords: Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families
Collection: 19th International Conference on Types for Proofs and Programs (TYPES 2013)
Issue Date: 2014
Date of publication: 25.07.2014

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