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.

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.

License

BSD License

History

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.

Topics

Session Launchbury

Depends on

Used by

Cite

× 
@article{Launchbury-AFP,
  author  = {Joachim Breitner},
  title   = {The Correctness of Launchbury's Natural Semantics for Lazy Evaluation},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2013},
  note    = {\url{https://isa-afp.org/entries/Launchbury.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: