一句话：为 CakeML 编译器设计支持函数调用优化的中间语言语义，并在 HOL4 中验证其编译步骤。
在 CakeML 编译器中，函数调用的高效编译与验证是一大挑战。本文设计了一种中间语言（IL），并为其定义形式语义，以支持经过验证的高效函数调用编译。所实现的验证编译步骤包括：批量处理多个柯里化参数、检测对静态已知函数的调用，以及特化无自由变量的已知函数调用。最后，论文验证了向更低层 IL 的翻译，该层仅支持封闭的一阶函数。这些步骤与 OCaml 等编译器中的优化类似。整个开发在 HOL4 定理证明器中完成，表明所提出的验证技术在此规模下切实可行，为编译器验证提供了可扩展的语义设计与证明方法。
We have designed an intermediate language (IL) for the CakeML compiler that supports the verified, efficient compilation of functions and calls. Verified compilation steps include batching of multiple curried arguments, detecting calls to statically known functions, and specialising calls to known functions with no free variables. Finally, we verify the translation to a lower-level IL that only supports closed, first-order functions. These compilation steps resemble those found in other compilers (especially OCaml). Our contribution here is the design of the semantics of the IL, and the demonstration that our verification techniques over this semantics work well in practice at this scale. The entire development was carried out in the HOL4 theorem prover.
@article{OwensNKMT17,
title = {Verifying efficient function calls in CakeML},
author = {Scott Owens and Michael Norrish and Ramana Kumar and Magnus O. Myreen and Yong Kiam Tan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110262}
}