Inductive-data-type systems

DOI10.1016/S0304-3975(00)00347-9zbMath0992.68121WikidataQ127972148 ScholiaQ127972148MaRDI QIDQ5958292

Frédéric Blanqui, Mitsuhiro Okada, Jean-Pierre Jouannaud

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

inductive typeshigher-order rewritingrecursive definitionsstrong normalizationtyped lambda-calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65) Grammars and rewriting systems (68Q42)

Related Items (16)

Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ An initial algebra approach to term rewriting systems with variable binders ⋮ Size-based termination of higher-order rewriting ⋮ Normal Higher-Order Termination ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Strong normalisation in two Pure Pattern Type Systems ⋮ Unnamed Item ⋮ The Computability Path Ordering: The End of a Quest ⋮ Expression reduction systems with patterns ⋮ Termination checking with types ⋮ Remarks on Isomorphisms of Simple Inductive Types ⋮ Semantic foundations for generalized rewrite theories ⋮ Unnamed Item ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics

Uses Software

• Automath

Cites Work

• Higher-order rewrite systems and their confluence
• Polymorphic rewriting conserves algebraic strong normalization
• Combinatory reduction systems: Introduction and survey
• Abstract data type systems
• Specification and proof in membership equational logic
• Combinators, \(\lambda\)-terms and proof theory
• Modularity of strong normalization in the algebraic-λ-cube
• Linear unification of higher-order patterns
• A logic programming language with lambda-abstraction, function variables, and simple unification
• Intensional interpretations of functionals of finite type I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Inductive-data-type systems