Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name
Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name
复制标题
DOI：
10.1007/978-3-319-90686-7_1
复制
发表时间：
2018-05
期刊：
影响因子：
--
通讯作者：
Masayuki Mizuno;Eijiro Sumii
中科院分区：
文献类型：
--
作者：
Masayuki Mizuno;Eijiro Sumii
我们形式化了微积分的按需调用评估（没有递归绑定），并使用Coq证明助手证明了它与按名调用的对应性。长期以来，人们一直认为，非严格语言的高层抽象（即按名调用评估）和它们的实际按需调用实现之间存在差距。虽然一些证明已经给出了弥合这一差距，他们不一定适合严格的，机械化的验证，因为使用了一个全球性的堆，“基于图形”的技术，或“显着减少”。我们的技术贡献是双重的：（1）我们给出了一个基于两种形式标准化的简单证明，采用de Bruijn指标表示（非递归）变量绑定沿着Ariola和Felleisen的小步语义，和（2）我们设计了一种技术，通过消除评估上下文的概念来显着简化形式化-这被认为是按需调用演算的关键-从定义。
We formalize the call-by-need evaluation of-calculus (with no recursive bindings) and prove its correspondence with call-by-name, using the Coq proof assistant.It has been long argued that there is a gap between the high-level abstraction of non-strict languages—namely,call-by-nameevaluation—and their actualcall-by-needimplementations. Although a number of proofs have been given to bridge this gap, they are not necessarily suitable for stringent, mechanized verification because of the use of a global heap, “graph-based” techniques, or “marked reduction”. Our technical contributions are twofold: (1) we give a simpler proof based on two forms of standardization, adopting de Bruijn indices for representation of (non-recursive) variable bindings along with Ariola and Felleisen’s small-step semantics, and (2) we devise a technique to significantly simplify the formalization by eliminating the notion of evaluation contexts—which have been considered essential for the call-by-need calculus—from the definitions.