This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC),an extension of the Calculus of Constructions by inductive data types.CAC generalizes inductive types equipped with higher-order primitive recursion,by providing definitions of functions by pattern-matching which capture recursor definitions for arbitrary non-dependent and non-polymorphic inductive types satisfying a strictly positivity condition.CAC dependent types and higher-order rewrite rules.Full proofs are available at http://www.lri.fr/-blanqui/publis/rta99full.ps.gz.
展开▼