A new verified compiler backend for CakeML
A new verified compiler backend for CakeML
复制标题
CakeML 的新的经过验证的编译器后端
DOI：
10.1145/2951913.2951924
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Tan Y
中科院分区：
文献类型：
--
作者：
Tan Y
我们已经为CakeML开发并机械地验证了一个新的编译器后端。我们的新编译器具有一系列中间语言，允许它增量地编译掉高级功能，并允许在正确的语义细节级别进行验证。在这方面，它类似于用于严格函数式语言的主流(未经验证)编译器。编译器支持高效的Currated多参数函数、可配置的数据表示、展开调用堆栈的异常、寄存器分配等。该编译器面向多种体系结构：x86-、ARMv6、ARMv8、MIPS-和RISC-V。本文给出了编译器的总体结构，包括它的12种中间语言，并说明了它们是如何组合在一起的。我们特别关注寄存器分配器和垃圾收集器的验证以及内存表示之间的交互。整个开发是在HOL4定理证明器中进行的。
We have developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V.In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations. The entire development has been carried out within the HOL4 theorem prover.
登录
查看更多内容
DOI：
--
发表时间：
2010
期刊：
European Symposium on Programming
影响因子：
--
作者：
Sandrine Blazy;Benoît Robillard;A. Appel
通讯作者：
A. Appel
用于非纯函数语言的经过验证的编译器
DOI：
--
发表时间：
2010
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
Pilsner：用于高阶命令式语言的组合验证编译器
DOI：
--
发表时间：
2015
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Georg Neis;C. Hur;Jan;Craig McLaughlin;Derek Dreyer;Viktor Vafeiadis
通讯作者：
Viktor Vafeiadis
影响因子：
1.3
作者：
Barthe, Gilles;Demange, Delphine;Pichardie, David
通讯作者：
Pichardie, David
COGENT：功能系统语言的认证编译
DOI：
--
发表时间：
2016
期刊：
arXiv.org
影响因子：
--
作者：
Liam O'Connor;C. Rizkallah;Zilin Chen;Sidney Amani;Japheth Lim;Yutaka Nagashima;Thomas Sewell;A. Hixon;G. Keller;Toby C. Murray;Gerwin Klein
通讯作者：
Gerwin Klein