Adding algebraic rewriting to the untyped lambda calculus

DOI10.1016/0890-5401(92)90064-MMaRDI QIDQ1207945zbMATH OpenFDO

Authors Daniel J. Dougherty

Publication date 16 May 1993

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

zbMATH Keywords

confluenceterminationpolymorphic lambda calculusalgebraic rewritinguntyped lambda calculus

Mathematics Subject Classification ID

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

Recommendations

• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Applying universal algebra to lambda calculus
• scientific article; zbMATH DE number 1499090
• scientific article; zbMATH DE number 431764
• Confluence of the lambda calculus with left-linear algebraic rewriting
• A typed, algebraic, computational lambda-calculus
• scientific article; zbMATH DE number 2185664
• Semantics of a typed algebraic lambda-calculus
• Extending the lambda-calculus with unbind and rebind

Cites work

• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 4124996 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Modular aspects of properties of term rewriting systems related to normal forms
• On termination of the direct sum of term-rewriting systems
• On the Church-Rosser property for the direct sum of term rewriting systems
• Termination for the direct sum of left-linear term rewriting systems
• Termination of rewriting
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• The calculus of constructions
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(25)

• Total unfolding: theory and applications
• scientific article; zbMATH DE number 2044492 (Why is no real title available?)
• A simplifier for untyped lambda expressions
• A domain model characterising strong normalisation
• Nominal rewriting
• Abstract data type systems
• Confluence via strong normalisation in an algebraic \(\lambda\)-calculus with rewriting
• On the confluence of lambda-calculus with conditional rewriting
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• The algebraic lambda calculus
• scientific article; zbMATH DE number 6712184 (Why is no real title available?)
• A combinatory logic approach to higher-order E-unification
• scientific article; zbMATH DE number 445155 (Why is no real title available?)
• Normal forms in combinatory logic
• Polymorphic rewriting conserves algebraic confluence
• scientific article; zbMATH DE number 4124996 (Why is no real title available?)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• An insertion operator preserving infinite reduction sequences
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• A framework for defining logical frameworks
• Confluence of the lambda calculus with left-linear algebraic rewriting
• The vectorial \(\lambda\)-calculus
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• On modular properties of higher order extensional lambda calculi
• The Computability Path Ordering: The End of a Quest

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1207945)