Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec

DOI10.1016/j.ipl.2011.04.011zbMath1260.68075WikidataQ124810604 ScholiaQ124810604MaRDI QIDQ1944119

Elena Machkasova, Manfred Schmidt-Schauss, David Sabel

Publication date: 4 April 2013

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2011.04.011

zbMATH Keywords

formal semantics; programming calculi; program correctness; contextual semantics

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q55: Semantics in the theory of computing

Related Items

Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report), Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi

Uses Software

• Fudgets

Cites Work

• Unnamed Item
• Unnamed Item
• On generic context lemmas for higher-order calculi with sharing
• Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi
• Erratic Fudgets: A semantic theory for an embedded coordination language
• The expressive power of indeterminate primitives in asynchronous computation
• A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations
• Safety of Nöcker's strictness analysis
• A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case
• Equivalence in functional languages with effects
• Amb Breaks Well-Pointedness, Ground Amb Doesn't
• Simulation in the call-by-need lambda-calculus with letrec