HOL-#lambda##of algebraic constructions#Frederic Blanqui; Jean-Pierre Jouannaud

摘要

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