HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/inria-00105655
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Wednesday, October 11, 2006 - 6:09:06 PM
Last modification on : Friday, February 4, 2022 - 3:22:48 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 5:47:55 PM

Files

Identifiers

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⟩

Share

Metrics

Record views

72

Files downloads

123