Combining algebraic rewriting, extensional lambda calculi, and fixpoints

DOI10.1016/S0304-3975(96)00121-1zbMATH Open0874.68158MaRDI QIDQ1349901FDOQ1349901

Authors: Roberto Di Cosmo, Delia Kesner 

Publication date: 27 February 1997

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

Recommendations

• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Adding algebraic rewriting to the untyped lambda calculus
• On modular properties of higher order extensional lambda calculi
• Publication:4205074

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Combinatory reduction systems: Introduction and survey
• Title not available (Why is that?)
• Title not available (Why is that?)
• Developing developments
• Title not available (Why is that?)
• Polymorphic rewriting conserves algebraic strong normalization
• Title not available (Why is that?)
• 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
• On the implementation of abstract data types by programming language constructs
• Polymorphic rewriting conserves algebraic confluence
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (16)

• Foundations of Software Science and Computation Structures
• Adding algebraic rewriting to the untyped lambda calculus
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• The simple type theory of normalisation by evaluation
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• On modular properties of higher order extensional lambda calculi
• Logical foundations for hybrid type-logical grammars
• Abstract data type systems
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• On the power of simple diagrams
• An insertion operator preserving infinite reduction sequences
• Termination of combined (rewrite and λ-calculus) systems
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Simulating expansions without expansions
• Canonicity of proofs in constructive modal logic

This page was built for publication: Combining algebraic rewriting, extensional lambda calculi, and fixpoints

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