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