Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)

Amin Timany 1 Matthieu Sozeau 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
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 : · · ·. 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.
Liste complète des métadonnées

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-01615123
Contributor : Matthieu Sozeau <>
Submitted on : Tuesday, January 23, 2018 - 10:53:44 AM
Last modification on : Thursday, February 21, 2019 - 10:31:47 AM
Document(s) archivé(s) le : Thursday, May 24, 2018 - 10:39:38 AM

File

consistency.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01615123, version 2

Citation

Amin Timany, Matthieu Sozeau. Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). [Research Report] RR-9105, KU Leuven, Belgium; Inria Paris. 2017, pp.30. ⟨hal-01615123v2⟩

Share

Metrics

Record views

304

Files downloads

140