@inproceedings{40c8aa24723843e1878dea0a4cd4c4bc,

title = "Simulation in the call-by-need lambda-calculus with letrec",

abstract = "This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.",

keywords = "Bisimulation, Call-by-need, Contextual equivalence, Lambda calculus, Letrec, Semantics",

author = "Manfred Schmidt-Schauss and David Sabel and Elena Machkasova",

year = "2010",

month = dec,

day = "1",

language = "English (US)",

isbn = "9783939897187",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

pages = "295--310",

booktitle = "Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010",

note = "21st International Conference on Rewriting Techniques and Applications, RTA 2010 ; Conference date: 11-07-2010 Through 13-07-2010",

}