Inductive types in the Calculus of Algebraic Constructions
<|reference_start|>Inductive types in the Calculus of Algebraic Constructions: 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.<|reference_end|>
@article{blanqui2006inductive,
    title={Inductive types in the Calculus of Algebraic Constructions},
    author={Fr'ed'eric Blanqui (INRIA Lorraine - LORIA)},
    journal={Fundamenta Informaticae 65, 1-2 (2005) 61-86},
    year={2006},
    number={Journal version of TLCA'03},
    archivePrefix={arXiv},
    eprint={cs/0610073},
    primaryClass={cs.LO}
}