Adding algebraic rewriting to the untyped lambda calculus

DOI10.1016/0890-5401(92)90064-MzbMath0769.68058MaRDI QIDQ1207945

Daniel J. Dougherty

Publication date: 16 May 1993

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

polymorphic lambda calculusconfluenceterminationalgebraic rewritinguntyped lambda calculus

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (14)

Unnamed Item ⋮ Nominal rewriting ⋮ Normal forms in combinatory logic ⋮ On modular properties of higher order extensional lambda calculi ⋮ Abstract data type systems ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Linear-algebraic λ-calculus: higher-order, encodings, and confluence. ⋮ The Computability Path Ordering: The End of a Quest ⋮ A combinatory logic approach to higher-order E-unification ⋮ A domain model characterising strong normalisation ⋮ The vectorial \(\lambda\)-calculus ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ A Framework for Defining Logical Frameworks ⋮ Total unfolding: theory and applications

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Termination of rewriting
• The calculus of constructions
• On termination of the direct sum of term-rewriting systems
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Modular aspects of properties of term rewriting systems related to normal forms
• Termination for the direct sum of left-linear term rewriting systems
• On the Church-Rosser property for the direct sum of term rewriting systems

This page was built for publication: Adding algebraic rewriting to the untyped lambda calculus