The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

Title:	The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
Author:	Joachim Breitner (joachim /at/ cis /dot/ upenn /dot/ edu)
Submission date:	2013-01-31
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".
BibTeX:	@article{Launchbury-AFP, author = {Joachim Breitner}, title = {The Correctness of Launchbury's Natural Semantics for Lazy Evaluation}, journal = {Archive of Formal Proofs}, month = jan, year = 2013, note = {\url{https://isa-afp.org/entries/Launchbury.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	FinFun, Nominal2
Used by:	Call_Arity
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.