The Calculus of Algebraic Constructions

This paper is concerned with the foundations of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions by inductive data types. CAC generalize inductive types equipped with primitive recursion of higher-type, by providing definitions of functions by pattern matching which capture recursor definitions for arbitrary non-dependent inductive types satisfying the positivity condition. CAC also generalizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules.

extended abstract

full paper