一句话：为已验证的 CakeML 编译器加入 Eval 原语，实现运行时代码求值与动态执行，并支持首个可验证的 LCF 风格定理证明器运行时环境。
本文扩展了经过形式化验证的 CakeML 编译器，引入新的语言原语 Eval，使程序能够在运行时求值新的 CakeML 语法。该实现支持一种雄心勃勃的运行时编译与动态执行形式：原有代码与动态加入的代码可以共享高阶值并相互递归调用。据作者所知，这是首个能够支持标准 LCF 风格定理证明器设计的可验证运行时环境。为支持动态计算语义而修改现代 CakeML 编译器流水线及其证明是一项庞大的工程。论文回顾了项目中的设计决策、证明技术与证明工程经验，并指出了若干意外出现的复杂问题。
We have extended the verified CakeML compiler with a new language primitive, Eval, which permits evaluation of new CakeML syntax at runtime. This new implementation supports an ambitious form of compilation at runtime and dynamic execution, where the original and dynamically added code can share (higher-order) values and recursively call each other. This is, to our knowledge, the first verified run-time environment capable of supporting a standard LCF-style theorem prover design. Modifying the modern CakeML compiler pipeline and proofs to support a dynamic computation semantics was an extensive project. We review the design decisions, proof techniques, and proof engineering lessons from the project, and highlight some unexpected complications.
@article{paperbot2011,
title = {Cakes That Bake Cakes: Dynamic Computation in CakeML},
author = {Thomas Sewell and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar and Alexander Mihajlovic and Oskar Abrahamsson and Scott Owens},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591266}
}