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 also generalizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules. Full proofs are available at http://www.lri.fr/~blanqui/publis/rta99full.ps.gz.
CITATION STYLE
Blanqui, F., Jouannaud, J. P., & Okada, M. (1999). The calculus of algebraic constructions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1631, pp. 301–316). Springer Verlag. https://doi.org/10.1007/3-540-48685-2_25
Mendeley helps you to discover research relevant for your work.