The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

Joachim Breitner 🌐

January 31, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


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


Session Launchbury