  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.
