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

DOI10.1007/3-540-58201-0_90zbMath1418.68112OpenAlexW1589742942MaRDI QIDQ4632448

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

strong normalizationlambda-calculusreduction rulereduction sequencemodular property

Mathematics Subject Classification ID

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

Related Items

Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract), Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Developing developments, Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Polymorphic rewriting conserves algebraic confluence
• On the semantics of the universal quantifier
• Simulating expansions without expansions
• A confluent reduction for the extensional typed λ-calculus with pairs, sums, recursion and terminal object
• The virtues of eta-expansion
• Some lambda calculi with categorical sums and products