The adequacy of Launchbury's natural semantics for lazy evaluation*. (3rd January 2018)

• Record Type: Journal Article
• Authors: BREITNER, JOACHIM
• Is Part Of: Journal of functional programming. Volume 28(2018)
• Publication Date: 2018-01-03
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796817000144
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: In his seminal paper "A Natural Semantics for Lazy Evaluation", John Launchbury proves his semantics correct with respect to a denotational semantics, and outlines a proof of adequacy. Previous attempts to rigorize the adequacy proof, which involves an intermediate natural semantics and an intermediate resourced denotational semantics, have failed. We devised a new, direct proof that skips the intermediate natural semantics. It is the first rigorous adequacy proof of Launchbury's semantics. We have modeled our semantics in the interactive theorem prover Isabelle and machine-checked our proofs. This does not only provide a maximum level of rigor, but also serves as a tool for further work, such as a machine-checked correctness proof of a compiler transformation.