一句话：在 Isabelle 中机器验证 Launchbury 惰性求值自然语义的 adequacy，首次给出严格证明。
Launchbury 在 1993 年提出惰性求值的自然语义，并相对指称语义证明了其正确性，但仅概述了 adequacy（充分性）证明；此前将其严格化的尝试依赖中间自然语义和带资源的指称语义，均未成功。本文给出一种新的直接证明，绕过中间自然语义，首次严格证明了 Launchbury 语义的 adequacy。作者在交互式定理证明器 Isabelle 中形式化该语义并机器检查全部证明，从而提供最高级别的严谨性，同时为后续工作（如编译器变换的正确性证明）提供了可复用的机器验证基础。
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.
DOI 原文 ·
@article{paperbot327,
title = {The adequacy of Launchbury's natural semantics for lazy evaluation},
author = {JOACHIM BREITNER},
journal = {Journal of Functional Programming},
volume = {28},
year = {2018},
doi = {10.1017/s0956796817000144}
}