Skip to Main content Skip to Navigation
Conference papers

The Calculus of Algebraic Constructions

Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Monday, May 26, 2008 - 2:54:04 PM
Last modification on : Sunday, June 26, 2022 - 11:48:16 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 4:37:40 PM


Files produced by the author(s)


  • HAL Id : inria-00105545, version 2
  • ARXIV : cs/0610063



Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada. The Calculus of Algebraic Constructions. Rewriting Techniques and Applications, 10th International Conference, RTA-99, Jul 1999, Trento, Italy. ⟨inria-00105545v2⟩



Record views


Files downloads