|
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{http://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.
|
|