Inductive types in the Calculus of Algebraic Constructions

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In a previous work, we proved that an important part of the Calculus of Inductive Constructions (CIC), the basis of the Coq proof assistant, can be seen as a Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In this paper, we prove that almost all CIC can be seen as a CAC, and that it can be further extended with non-strictly positive types and inductive-recursive types together with non-free constructors and pattern-matching on defined symbols.
Type de document :
Article dans une revue
Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2005, 65 (1-2), pp.61-86
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00105655
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 18:09:06
Dernière modification le : jeudi 8 février 2018 - 11:32:01
Document(s) archivé(s) le : mardi 6 avril 2010 - 17:47:55

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2005, 65 (1-2), pp.61-86. 〈inria-00105655〉

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

109