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 almost all of the Calculus of Inductive Constructions (CIC), which is 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 not only prove that CIC as a whole can be seen as a CAC, but also that it can be extended with non-free constructors, pattern-matching on defined symbols, non-strictly positive types and inductive-recursive types.<|reference_end|>
@article{blanqui2006inductive,
    title={Inductive types in the Calculus of Algebraic Constructions},
    author={Fr'ed'eric Blanqui (LIX)},
    journal={Dans Typed Lambda Calculi and Applications, 6th International
  Conference, TLCA 2003 2701 (2003)},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0610070},
    primaryClass={cs.LO}
}