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.FSCD.2018.29
URN: urn:nbn:de:0030-drops-91991
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9199/
Go to the corresponding LIPIcs Volume Portal

Timany, Amin ; Sozeau, Matthieu

Cumulative Inductive Types In Coq

pdf-format:
LIPIcs-FSCD-2018-29.pdf (0.6 MB)

Abstract

In order to avoid well-known paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type_0 : Type_1 : *s. Such type systems are called cumulative if for any type A we have that A : Type_i implies A : Type_{i+1}. The Predicative Calculus of Inductive Constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system. In this paper we present the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) which extends the cumulativity relation to inductive types. We discuss cumulative inductive types as present in Coq 8.7 and their application to formalization and definitional translations.

BibTeX - Entry

@InProceedings{timany_et_al:LIPIcs:2018:9199,
  author =	{Amin Timany and Matthieu Sozeau},
  title =	{{Cumulative Inductive Types In Coq}},
  booktitle =	{3rd International Conference on Formal Structures for  Computation and Deduction (FSCD 2018)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9199},
  URN =		{urn:nbn:de:0030-drops-91991},
  doi =		{10.4230/LIPIcs.FSCD.2018.29},
  annote =	{Keywords: Coq, Proof Assistants, Inductive Types, Universes, Cumulativity}
}

Keywords: Coq, Proof Assistants, Inductive Types, Universes, Cumulativity
Collection: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue Date: 2018
Date of publication: 04.07.2018

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