# 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