一句话：首个端到端机器验证的惰性函数式语言编译器，将 PureLang 编译到机器码并在 HOL4 中完成正确性证明。
惰性函数式语言的编译正确性此前缺乏从源语言到机器码的端到端机器验证。本文提出 PureCake，一个在 HOL4 交互式定理证明器中开发的已验证编译器，面向 PureLang——一种 Haskell 风格、缩进敏感、带单子效应的纯惰性函数式语言，其基于约束的 Hindley-Milner 类型系统保证安全执行。作者从 PureLang 的操作语义出发推导了可靠的等式推理原则，显著简化了部分证明；编译器包含多趟优化以有效处理现实的惰性编程惯用法，并以 CakeML 为目标后端，通过组合其已验证编译器实现端到端编译。最终，作者在 HOL4 中机械化证明了从 PureLang 到机器码的端到端正确性，这是任意惰性语言的首个此类结果。
We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-to-end correctness for the compilation of PureLang down to machine code---the first such result for any lazy language---by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.
@article{paperbot1950,
title = {PureCake: A Verified Compiler for a Lazy Functional Language},
author = {Hrutvik Kanabar and Samuel Vivien and Oskar Abrahamsson and Magnus O. Myreen and Michael Norrish and Johannes Åman Pohjola and Riccardo Zanetti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591259}
}