Inductive types in the Calculus of Algebraic Constructions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Fundamenta Informaticae Année : 2005

Inductive types in the Calculus of Algebraic Constructions

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (246.92 Ko) Télécharger le fichier
Loading...

Dates et versions

inria-00105655 , version 1 (11-10-2006)

Identifiants

Citer

Frédéric Blanqui. Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae, 2005, 65 (1-2), pp.61-86. ⟨inria-00105655⟩
76 Consultations
125 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More