Inductive types in the Calculus of Algebraic Constructions

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 dened 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 dened symbols.

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Frédéric Blanqui
• Keywords: Calculus, Constructions, CORR 2006, Education, Proof Assistant Coq