Combining algebraic rewriting, extensional lambda calculi, and fixpoints

DOI10.1016/S0304-3975(96)00121-1zbMath0874.68158MaRDI QIDQ1349901

Roberto Di Cosmo, Delia Kesner

Publication date: 27 February 1997

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

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Logical foundations for hybrid type-logical grammars, Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract), On the power of simple diagrams, 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, An insertion operator preserving infinite reduction sequences, The Simple Type Theory of Normalisation by Evaluation, Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On the implementation of abstract data types by programming language constructs
• Polymorphic rewriting conserves algebraic strong normalization
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• Combinatory reduction systems: Introduction and survey
• Polymorphic rewriting conserves algebraic confluence
• Developing developments
• Simulating expansions without expansions
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• The virtues of eta-expansion
• Some lambda calculi with categorical sums and products