arXiv 1503.086652015-03cs.PL

一种线性一阶函数中间语言

A Linear First-Order Functional Intermediate Language for Verified Compilers

Sigurd Schneider, Gert Smolka, Sebastian Hack

备注：: Addressed comments from reviewers (ITP 2015): (1) Added discussion of a paper in related work (2) Added definition of renamed-apart in appendix (3) Formulation changes in a coupe of places

摘要：

我们提出了线性一阶中间语言IL验证编译器。IL是一种函数式语言，可以调用非确定性环境。我们给IL条款的第二个，命令式语义解释，并获得一个寄存器转移语言。对于命令式解释，我们建立了活变量的概念。基于活变量，我们制定了一个可判定的属性称为一致性，确保功能和命令的解释一个术语相吻合。我们制定了一个寄存器分配算法的IL，并证明其正确性。该算法将一个函数式IL程序转换为一个等价的命令式IL程序。正确性来自于这样一个事实，即算法在一致地重命名局部变量后达到了一个连贯的程序。我们证明了初始程序中的最大活变量数限制了最终相干程序中不同变量的数量。整个开发都在Coq中正式化。

英文摘要：

We present the linear first-order intermediate language IL for verified compilers. IL is a functional language with calls to a nondeterministic environment. We give IL terms a second, imperative semantic interpretation and obtain a register transfer language. For the imperative interpretation we establish a notion of live variables. Based on live variables, we formulate a decidable property called coherence ensuring that the functional and the imperative interpretation of a term coincide. We formulate a register assignment algorithm for IL and prove its correctness. The algorithm translates a functional IL program into an equivalent imperative IL program. Correctness follows from the fact that the algorithm reaches a coherent program after consistently renaming local variables. We prove that the maximal number of live variables in the initial program bounds the number of different variables in the final coherent program. The entire development is formalized in Coq.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

摘要：

英文摘要：

相关论文