Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations

Since Val Tannen's pioneering work on the combination of simply-typed λ-calculus and rst-order rewriting [11], many authors have contributed to this subject by extending it to richer typed λ-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are dened by oriented higher-order equations. This kind of denitions subsumes usual inductive denitions, is easier to write and provides more automation. On the other hand, checking that such user-dened rewrite rules, when combined with β-reduction, are strongly normalizing and conuent, and preserve the decidability of type-checking, is more dicult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of sized types studied by several authors in the simpler framework of MLlike languages, and prov...

• Type: Conference
• Year: 2005
• Where: CSL
• Authors: Frédéric Blanqui
• Keywords: Algebraic Constructions, CSL 2005, Tannen's Pioneering Work, Usual Inductive Denitions