Simulating expansions without expansions

DOI10.1017/S0960129500000505MaRDI QIDQ4322432zbMATH OpenFDO

Authors Roberto Di Cosmo, Delia Kesner

Publication date 18 February 1996

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129500000505

zbMATH Keywords

bounded recursionconfluenceexpansion rulesextensional equalitiesrewriting systemstrong normalizationsumstyped \(\lambda\)-calculusunbounded recursion

Mathematics Subject Classification ID

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

Recommendations

• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• scientific article; zbMATH DE number 2185658
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Extensional Rewriting with Sums

Cites work

• An algebraic interpretation of the K-calculus; and an application of a labelled -calculus
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• On the implementation of abstract data types by programming language constructs
• Strong normalization for typed terms with surjective pairing
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(19)

• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Simulation without mediator
• Developing developments
• A local graph-rewriting system for deciding equality in sum-product theories
• Normal higher-order termination
• scientific article; zbMATH DE number 2185658 (Why is no real title available?)
• Extensional Rewriting with Sums
• scientific article; zbMATH DE number 1332635 (Why is no real title available?)
• Simulating without Negation
• scientific article; zbMATH DE number 1114357 (Why is no real title available?)
• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• Some lambda calculi with categorical sums and products
• On the power of simple diagrams
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• Call-by-name extensionality and confluence
• Extensional proofs in a propositional logic modulo isomorphisms
• Rewriting with extensional polymorphic \(\lambda \)-calculus
• Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus

This page was built for publication: Simulating expansions without expansions

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