Launchbury的自然语义对惰性求值的正确性
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
摘要：
John Launchbury在他的开创性论文“A Natural Semantics for Lazy Evaluation”中证明了他关于指称语义的语义正确性。我们对证明进行了机器检查，发现它失败了，并提供了两种方法来修复它：一种是通过显式堆栈修改自然语义，另一种是通过调整堆的指称语义。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
