Sonstiges: The Correctness of Launchbury's Natural Semantics for Lazy Evaluation

[breitner14launchburycorrect]

Joachim Breitner, The Correctness of Launchbury's Natural Semantics for Lazy Evaluation, May 2014.

Zusammenfassung

In his seminal paper "A Natural Semantics for Lazy Evaluation", John Launchbury proves his semantics correct with respect to a denotational semantics. We machine-checked the proof and found it to fail, and provide two ways to fix it: One by taking a detour via a modified natural semantics with an explicit stack, and one by adjusting the denotational semantics of heaps.

Download

[Link]

BibTeX

@misc{breitner14launchburycorrect,
  title = {The Correctness of Launchbury's Natural Semantics for Lazy Evaluation},
  year = {2014},
  month = may,
  journal = {ArXiv e-prints},
  author = {Joachim Breitner},
  url = {http://arxiv.org/abs/1405.3099},
}

Institutsinterne Autoren

Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner