The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

TL;DR

This paper examines Launchbury's natural semantics for lazy evaluation, identifies errors in its correctness proof, and proposes two fixes involving a modified semantics with an explicit stack and adjusted denotational semantics.

Contribution

It provides the first machine-checked verification of Launchbury's semantics and offers two novel corrections to ensure its correctness.

Findings

The original proof of correctness contains errors.

Two methods are proposed to fix the proof: one using an explicit stack, another adjusting denotational semantics.

The corrected semantics are validated to be consistent and correct.

Abstract

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.