In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), the basis of the proof assistant Coq, 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 CIC as a whole can be seen as a CAC, and that it can be extended with nonstrictly positive types and inductive-recursive types together with nonfree constructors and pattern-matching on defined symbols. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Blanqui, F. (2003). Inductive types in the Calculus of Algebraic Constructions. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2701, 46–59. https://doi.org/10.1007/3-540-44904-3_4
Mendeley helps you to discover research relevant for your work.