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
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, October 11, 2006 - 6:09:06 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 5:47:55 PM





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⟩



Record views


Files downloads