Inductive types in the Calculus of Algebraic Constructions

TL;DR

This paper demonstrates that most of the Calculus of Inductive Constructions (CIC), foundational to Coq, can be represented as a Calculus of Algebraic Constructions (CAC), and extends it with advanced type features.

Contribution

It shows that CIC can be modeled as a CAC and introduces extensions with non-strictly positive types, inductive-recursive types, and complex pattern-matching capabilities.

Findings

Most of CIC can be represented as a CAC

Extended CAC with non-strictly positive and inductive-recursive types

Enhanced pattern-matching on defined symbols

Abstract

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.