Combining first order algebraic rewriting systems, recursion and extensional lambda calculi

DOI10.1007/3-540-58201-0_90MaRDI QIDQ4632448zbMATH OpenOpenAlexFDO

Authors Roberto Di Cosmo, Delia Kesner

Publication date 29 April 2019

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58201-0_90

zbMATH Keywords

lambda-calculusmodular propertyreduction rulereduction sequencestrong normalization

Mathematics Subject Classification ID

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

Recommendations

• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Simulating expansions without expansions
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• On modular properties of higher order extensional lambda calculi

Cites work

• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 3573844 (Why is no real title available?)
• scientific article; zbMATH DE number 512797 (Why is no real title available?)
• On the semantics of the universal quantifier
• Polymorphic rewriting conserves algebraic confluence
• Simulating expansions without expansions
• Some lambda calculi with categorical sums and products
• The virtues of eta-expansion

Cited in

(15)

• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Developing developments
• Compiling dyadic first-order specifications into map algebra
• Modularity of strong normalization in the algebraic-λ-cube
• scientific article; zbMATH DE number 1303339 (Why is no real title available?)
• scientific article; zbMATH DE number 512772 (Why is no real title available?)
• Simulating expansions without expansions
• On modular properties of higher order extensional lambda calculi
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• System F i
• scientific article; zbMATH DE number 6792369 (Why is no real title available?)
• Termination of combined (rewrite and λ-calculus) systems
• Rewriting with extensional polymorphic \(\lambda \)-calculus
• Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations

This page was built for publication: Combining first order algebraic rewriting systems, recursion and extensional lambda calculi

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