The Calculus of Algebraic Constructions
Fr\'ed\'eric Blanqui (LRI), Jean-Pierre Jouannaud (LRI), Mitsuhiro, Okada

TL;DR
This paper explores the foundations of the Calculus of Algebraic Constructions (CAC), an advanced type theory framework that extends the Calculus of Constructions with inductive data types, higher-order recursion, and dependent types.
Contribution
It introduces the formal foundations of CAC, enabling definitions of functions via pattern-matching for complex inductive types with higher-order recursion.
Findings
Defines a strictly positive condition for inductive types.
Provides a formal framework for pattern-matching and recursion.
Extends the calculus with dependent types and higher-order rewrite rules.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Database Systems and Queries
