Inductive-data-type Systems

Abstract

In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the "General Schema", which generalizes the usual recursor definitions for natural numbers and similar "basic inductive types". This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called "strictly positive", and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types.

Theoretical Computer Science (2002)

Cited by in corpus (12)

• Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility
• Higher-Order Termination: from Kruskal to Computability
• Type theory and rewriting
• Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers
• The unified higher-order dependency pair framework
• Partiality and Recursion in Higher-order Logic
• The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics
• Argument filterings and usable rules in higher-order rewrite systems
• Confluent terminating extensional lambda-calculi with surjective pairing and terminal type
• A static higher-order dependency pair framework
• On Quasi Ordinal Diagram Systems
• Effectful Programming in Declarative Languages with an Emphasis on Non-Determinism: Applications and Formal Reasoning