Inductive types in the Calculus of Algebraic Constructions

Issue title: Typed Lambda Calculi and Applications 2003, Selected Papers

Article type: Research Article

Authors: Blanqui, Frédéric

Affiliations: LORIA & INRIA 615 rue du Jardin Botanique, BP 101, 54602 Villers-lès-Nancy, France. blanqui@loria.fr

Note: [] Address for correspondence: LORIA & INRIA, 615 rue du Jardin Botanique, BP 101, 54602 Villers-lès-Nancy, France

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.

Journal: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 61-86, 2005