[PRL] [1405.3099] The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

[Mitchell Wand]

In his seminal paper "A Natural Semantics for Lazy Evaluation", John
Launchbury proves his semantics correct with respect to a denotational
semantics. We machine-checked the proof and found it to fail, and provide
two ways to fix it: One by taking a detour via a modified natural semantics
with an explicit stack, and one by adjusting the denotational semantics of
heaps.

http://arxiv.org/abs/1405.3099
-------------- next part --------------
HTML attachment scrubbed and removed