References & Citations
Computer Science > Programming Languages
Title: Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)
(Submitted on 11 Oct 2017 (v1), last revised 11 Mar 2020 (this version, v3))
Abstract: In order to avoid well-know 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$ : $\cdots$ . 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 and establish the soundness of the predicative calculus of cumulative inductive constructions (pCuIC) which extends the cumulativity relation to inductive types.
Submission history
From: Amin Timany [view email][v1] Wed, 11 Oct 2017 05:31:26 GMT (38kb)
[v2] Mon, 22 Jan 2018 11:53:50 GMT (38kb)
[v3] Wed, 11 Mar 2020 12:24:14 GMT (42kb)
Link back to: arXiv, form interface, contact.