Inductive types in the Calculus of Algebraic Constructions
Logic in Computer Science
2016-08-16 v1
Abstract
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.
Cite
@article{arxiv.cs/0610070,
title = {Inductive types in the Calculus of Algebraic Constructions},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:cs/0610070},
year = {2016}
}