The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

Joachim Breitner

31 January 2013

Abstract

In his seminal paper "Natural Semantics for Lazy Evaluation", John Launchbury proves his semantics correct with respect to a denotational semantics, and outlines an adequacy proof. We have formalized both semantics and machine-checked the correctness proof, clarifying some details. Furthermore, we provide a new and more direct adequacy proof that does not require intermediate operational semantics.

Change history

[2014-05-24] Added the proof of adequacy, as well as simplified and improved the existing proofs. Adjusted abstract accordingly. [2015-03-16] Booleans and if-then-else added to syntax and semantics, making this entry suitable to be used by the entry "Call_Arity".