Inductive types in the Calculus of Algebraic Constructions

Abstract : In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), which is the basis of the proof assistant Coq, 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 not only prove that CIC as a whole can be seen as a CAC, but also that it can be extended with non-free constructors, pattern-matching on defined symbols, non-strictly positive types and inductive-recursive types.
Type de document :
Communication dans un congrès
Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Jun 2003, Valencia, Spain. 2701, 2003, LNCS
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00105617
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 16:26:22
Dernière modification le : jeudi 10 mai 2018 - 02:06:40
Document(s) archivé(s) le : mardi 6 avril 2010 - 19:24:37

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. Inductive types in the Calculus of Algebraic Constructions. Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Jun 2003, Valencia, Spain. 2701, 2003, LNCS. 〈inria-00105617〉

Partager

Métriques

Consultations de la notice

102

Téléchargements de fichiers

102