A Semantic Account of Type-Directed Partial Evaluation
A Semantic Account of Type-Directed Partial Evaluation
复制标题
类型导向部分评估的语义解释
DOI：
10.7146/brics.v6i17.20074
复制
发表时间：
1999
影响因子：
3.4
通讯作者：
Andrzej Filinski
中科院分区：
文献类型：
--
作者：
Andrzej Filinski
我们正式将功能程序的部分评估视为方程理论中的归一化问题，并得出了一种基于类型的划分为标准化，以在这种情况下计算正常形式。然后，我们使用基于Kripke逻辑关系的语义参数来建立该算法的正确性。为了简单起见，结果是针对非严格的，纯粹的功能性语言的；但是，这些方法也直接适用于以ML样语言的方式说明和证明类型定向的部分评估的正确性。
We formally characterize partial evaluation of functional programs as a normalization problem in an equational theory, and derive a type-based normalization-by-evaluation algorithm for computing normal forms in this setting. We then establish the correctness of this algorithm using a semantic argument based on Kripke logical relations. For simplicity, the results are stated for a non-strict, purely functional language; but the methods are directly applicable to stating and proving correctness of type-directed partial evaluation in ML-like languages as well.