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.
Type de document :
Rapport
[Research Report] RR-9105, KU Leuven, Belgium; Inria Paris. 2017, pp.30
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01615123
Contributeur : Matthieu Sozeau <>
Soumis le : mardi 23 janvier 2018 - 10:53:44
Dernière modification le : vendredi 20 avril 2018 - 17:12:20

Fichier

consistency.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01615123, version 2

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-01615123v2〉

Partager

Métriques

Consultations de la notice

126

Téléchargements de fichiers

22