The Calculus of Algebraic Constructions

11 years 5 months ago
The Calculus of Algebraic Constructions
: 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 patternmatching which capture recursor definitions for arbitrary non-dependent and non-polymorphic inductive types satisfying a strictly positivity condition. CAC eralizes the first-order framework of abstract data types by providing dependent types and higher-order rewrite rules.
Frédéric Blanqui, Jean-Pierre Jouann
Added 11 Dec 2010
Updated 11 Dec 2010
Type Journal
Year 2006
Where CORR
Authors Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
Comments (0)