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

[Matthias Felleisen]

On May 22, 2014, at 7:32 AM, Mitchell Wand wrote:

> 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


I scanned the paper a while back. What's "seminal" about this paper? Are these mistakes serious enough to warrant a paper? It reminded me of a homework assignment in the early 1990s in my PL class when Dorai tex-ed a nice 2-page solution with every proof step included for what I thought was a plain exercise in denotational semantics. A couple of months later I encountered a short paper in TCS (by Allen Stoughton) on just this topic. Some things are so obvious they don't need papers. -- Matthias

-------------- next part --------------
HTML attachment scrubbed and removed