Skip to Main content Skip to Navigation
Reports

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
Résumé : Les théories des types d’ordre supérieur sont stratifiées afin d’éviter les paradoxes bien connus associés aux définitions circulaires. Elles utilisent une hiérarchie dénombrable d’univers (aussi appelé sortes), Type0 : Type1 : · · · . Ces systèmes de types sont appelés cumulatifs si pour tout type A on a A : Typei implique A : Typei+1. Le calcul prédicatif des constructions inductives (pCIC), qui forme la base de l’assistant de preuve Coq, est un tel système. Dans cet article, nous présentons une extension du calcul, dont nous prouvons la cohérence relative vis à vis de la théorie des ensembles. Ce nouveau calcul étend la relation de cumulativité aux types inductifs.
Complete list of metadatas

Cited literature [39 references]  Display  Hide  Download

https://hal.inria.fr/hal-01615123
Contributor : Matthieu Sozeau <>
Submitted on : Wednesday, May 13, 2020 - 12:44:10 PM
Last modification on : Saturday, May 16, 2020 - 3:45:12 AM

File

consistency.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01615123, version 3

Collections

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-01615123v3⟩

Share

Metrics

Record views

20

Files downloads

109