Verifying efficient function calls in CakeML
Verifying efficient function calls in CakeML
复制标题
验证 CakeML 中的高效函数调用
DOI：
10.1145/3110262
复制
发表时间：
2017
影响因子：
--
通讯作者：
Owens S
中科院分区：
文献类型：
--
作者：
Owens S
我们为CakeML编译器设计了一种中间语言（IL），它支持函数和调用的验证，高效编译。已验证的编译步骤包括对多个curry参数进行验证，检测对静态已知函数的调用，以及专门调用没有自由变量的已知函数。最后，我们验证转换到只支持封闭的一阶函数的低层IL。这些编译步骤类似于其他编译器（特别是OCaml）中的编译步骤。我们在这里的贡献是IL语义的设计，以及证明我们对该语义的验证技术在这种规模的实践中运行良好。整个开发都在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.
登录
查看更多内容
用于非纯函数语言的经过验证的编译器
DOI：
--
发表时间：
2010
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
A. Chlipala
通讯作者：
A. Chlipala
快速柯里化：push/enter 与 eval/apply 用于高阶语言
DOI：
--
发表时间：
2004
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
S. Marlow;S. Jones
通讯作者：
S. Jones
通过“混合”归纳定义的计算充分性
DOI：
--
发表时间：
1993
期刊：
Mathematical Foundations of Programming Semantics
影响因子：
--
作者：
A. Pitts
通讯作者：
A. Pitts
通过近似反向翻译进行完全抽象编译
DOI：
--
发表时间：
2015
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Dominique Devriese;Marco Patrignani;Frank Piessens
通讯作者：
Frank Piessens
Pilsner：用于高阶命令式语言的组合验证编译器
DOI：
--
发表时间：
2015
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Georg Neis;C. Hur;Jan;Craig McLaughlin;Derek Dreyer;Viktor Vafeiadis
通讯作者：
Viktor Vafeiadis