Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2017

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

Cohérence du Calcul Prédicatif des Constructions Inductives Cumulatives

Résumé

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.
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.
Fichier principal
Vignette du fichier
consistency.pdf (1003.58 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01615123 , version 1 (30-10-2017)
hal-01615123 , version 2 (23-01-2018)
hal-01615123 , version 3 (13-05-2020)

Identifiants

  • HAL Id : hal-01615123 , version 3

Citer

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.32. ⟨hal-01615123v3⟩
588 Consultations
536 Téléchargements

Partager

Gmail Facebook X LinkedIn More