arXiv:cs/0610073 [cs.LO]AbstractReferencesReviewsResources
Inductive types in the Calculus of Algebraic Constructions
Published 2006-10-12Version 1
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.
Comments: Journal version of TLCA'03
Journal: Fundamenta Informaticae 65, 1-2 (2005) 61-86
Categories: cs.LO
Keywords: algebraic constructions, inductive types, coq proof assistant, higher-order rewrite rules, important part
Tags: journal article
Related articles: Most relevant | Search more
arXiv:cs/0610070 [cs.LO] (Published 2006-10-11)
Inductive types in the Calculus of Algebraic Constructions
The Calculus of Algebraic Constructions
arXiv:2302.08837 [cs.LO] (Published 2023-02-17)
Type-Theoretic Signatures for Algebraic Theories and Inductive Types