一句话：介绍经 HOL4 机器验证的 CakeML 编译器后端设计、12 个中间语言、语义证明与自举。
本文介绍经验证的 CakeML 编译器后端。CakeML 是迄今最现实的函数式语言验证编译器之一，其架构用一系列中间语言逐层消除高层特性，使每个编译 pass 能在合适的语义粒度上验证。后端支持柯里化多参函数、可配置数据表示、高效异常和寄存器分配等优化，并生成 x86-64、ARMv6、ARMv8、MIPS-64 与 RISC-V 机器码。生成代码内含经验证运行时，包括分代复制垃圾收集器和任意精度算术库。论文阐述后端整体设计、12 个中间语言、语义与证明的组织方式，以及编译器如何在定理证明器逻辑内自举；全部开发在 HOL4 中完成。
Abstract The CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler’s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.
@article{paperbot726,
title = {The verified CakeML compiler backend},
author = {YONG KIAM TAN and MAGNUS O. MYREEN and RAMANA KUMAR and ANTHONY FOX and SCOTT OWENS and MICHAEL NORRISH},
journal = {Journal of Functional Programming},
volume = {29},
year = {2019},
doi = {10.1017/s0956796818000229}
}