Specifying the correctness of binding-time analysis
Specifying the correctness of binding-time analysis
复制标题
指定结合时间分析的正确性
DOI：
10.1145/158511.158614
复制
发表时间：
1993
影响因子：
1.1
通讯作者：
M. Wand
中科院分区：
文献类型：
--
作者：
M. Wand
莫根森（Mogensen）使用结合时间分析随后进行了专业化表现出非常紧凑的部分评估符，用于纯lambda演算。我们给出了该部分评估者的正确性标准，并证明其相对于此规范的正确性。我们表明，部分评估者（例如Futamura预测）的常规属性是该规范的后果。通过考虑流量分析及其合理的转换，该证明提出了将流量分析纳入经过验证的编译器的框架。
Mogensen has exhibited a very compact partial evaluator for the pure lambda calculus, using binding-time analysis followed by specialization. We give a correctness criterion for this partial evaluator and prove its correctness relative to this specification. We show that the conventional properties of partial evaluators, such as the Futamura projections, are consequences of this specification. By considering both a flow analysis and the transformation it justifies together, this proof suggests a framework for the incorporating flow analyses into verified compilers.