Compiling with continuations, correctly
Compiling with continuations, correctly
复制标题
正确地使用延续进行编译
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Anvay Grover
中科院分区：
文献类型：
--
作者：
Zoe Paraskevopoulou;Anvay Grover
在本文中，我们提出了一种新颖的模拟关系，用于证明程序转换的正确性，该关系结合了句法模拟和逻辑关系。特别是，我们建立了一种新型模拟图，它在源语言中使用小步或大步语义，在目标语言中使用非类型化、步索引逻辑关系。我们的技术提供了一种实用的解决方案，用于证明不保留源语言缩减的转换的语义保留。当转换生成新的绑定器名称时，这很常见，因此必须明确考虑 α 转换，或者当转换引入管理 Redexes 时。我们的技术不需要源语言的缩减来直接对应于目标语言的缩减。相反，我们强制执行较弱的语义预序概念，这足以表明语义对于整个程序和单独的编译都是保留的。因为我们的逻辑关系是传递的，所以我们可以以小步方式在中间程序状态之间转换，因此证明的形状类似于简单的小步模拟。我们使用这种技术来重新审视连续传递风格 (CPS) 转换的语义正确性，并演示它如何使我们能够克服与 α 转换和管理缩减相关的证明的众所周知的复杂性。此外，通过使用由与两个程序的资源消耗相关的不变量索引的逻辑关系，我们能够证明该转换保留了不同的行为，并且我们的 CPS 转换渐近地保留了源程序的运行时间。我们的结果在 Coq 证明助手中正式化。我们的连续传递样式转换是 Gallina（Coq 规范语言）的 CertiCoq 编译器的一部分。
In this paper we present a novel simulation relation for proving correctness of program transformations that combines syntactic simulations and logical relations. In particular, we establish a new kind of simulation diagram that uses a small-step or big-step semantics in the source language and an untyped, step-indexed logical relation in the target language. Our technique provides a practical solution for proving semantics preservation for transformations that do not preserve reductions in the source language. This is common when transformations generate new binder names, and hence α-conversion must be explicitly accounted for, or when transformations introduce administrative redexes. Our technique does not require reductions in the source language to correspond directly to reductions in the target language. Instead, we enforce a weaker notion of semantic preorder, which suffices to show that semantics are preserved for both whole-program and separate compilation. Because our logical relation is transitive, we can transition between intermediate program states in a small-step fashion and hence the shape of the proof resembles that of a simple small-step simulation. We use this technique to revisit the semantic correctness of a continuation-passing style (CPS) transformation and we demonstrate how it allows us to overcome well-known complications of this proof related to α-conversion and administrative reductions. In addition, by using a logical relation that is indexed by invariants that relate the resource consumption of two programs, we are able show that the transformation preserves diverging behaviors and that our CPS transformation asymptotically preserves the running time of the source program. Our results are formalized in the Coq proof assistant. Our continuation-passing style transformation is part of the CertiCoq compiler for Gallina, the specification language of Coq.
CertiCoq 的成分优化
影响因子：
--
作者：
Paraskevopoulou, Zoe;Li, John M.;Appel, Andrew W.
通讯作者：
Appel, Andrew W.
验证 CakeML 中的高效函数调用
影响因子：
--
作者：
Owens S
通讯作者：
Owens S