Skip to Main content Skip to Navigation
Conference papers

Cumulative Inductive Types in Coq

Amin Timany 1 Matthieu Sozeau 2, 3
3 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
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 : · · ·. 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01952037
Contributor : Matthieu Sozeau <>
Submitted on : Friday, January 4, 2019 - 2:16:49 PM
Last modification on : Saturday, April 11, 2020 - 1:57:47 AM
Long-term archiving on: : Friday, April 5, 2019 - 2:35:53 PM

File

LIPIcs-FSCD-2018-29.pdf
Files produced by the author(s)

Identifiers

Citation

Amin Timany, Matthieu Sozeau. Cumulative Inductive Types in Coq. FSCD 2018 - 3rd International Conference on Formal Structures for Computation and Deduction, Jul 2018, Oxford, United Kingdom. ⟨10.4230/LIPIcs.FSCD.2018.29⟩. ⟨hal-01952037⟩

Share

Metrics

Record views

181

Files downloads

527