Inductive types in the Calculus of Algebraic Constructions

TL;DR

This paper demonstrates that the Calculus of Inductive Constructions (CIC), foundational to Coq, can be fully represented as a Calculus of Algebraic Constructions (CAC) and extended with advanced features like non-free constructors and inductive-recursive types.

Contribution

It proves that CIC can be modeled as a CAC and extended with complex features such as non-free constructors, pattern-matching, and inductive-recursive types.

Findings

CIC can be fully represented as a CAC.

CIC can be extended with non-free constructors and pattern-matching.

CIC can incorporate inductive-recursive types.

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.