Formalizing a Correctness Property of a Type-Directed Partial Evaluator

Formalizing a Correctness Property of a Type-Directed Partial Evaluator
复制标题

形式化类型导向部分求值器的正确性属性

DOI：
10.1145/2541568.2541572
复制
发表时间：
2014
期刊：
Proc. of ACM SIGPLAN Workshop on Programming Language meets Program Verification
影响因子：
--
通讯作者：
Noriko Hirota and Kenichi Asai
Noriko Hirota and Kenichi Asai
中科院分区：
--
文献类型：
--
作者：
A.K.M. Mahfuzul Islam;Tohru Ishihara;and Hidetoshi Onodera;清水直;Noriko Hirota and Kenichi Asai

文献摘要

相似文献

本文介绍了我们在证明辅助工具CoQ中对按名字调用的Lambda演算的Danvy类型定向部分赋值器(TDPE)进行形式化的经验。遵循Coquand和Ilik之前的方法，我们将TDPE描述为类型规则相对于语义的完备性和合理性定理的组合。为了证明TDPE的正确性(即TDPE保留了语义)，我们在Filinski的基础上进一步定义了剩余语义和标准语义之间的逻辑关系。使用参数高阶抽象语法(PHOAS)可以实现简单的形式化，而不会受到在TDPE期间创建的新名称的干扰。由于PHOAS的高阶性质，它还要求我们手动证明与逻辑关系的主要引理相对应的核心性质，这在Coq中似乎很难证明。
This paper presents our experience of formalizing Danvy's type-directed partial evaluator (TDPE) for the call-by-name lambda calculus in the proof assistant Coq. Following the previous approach by Coquand and Ilik, we characterize TDPE as a composition of completeness and soundness theorems of typing rules with respect to the semantics. To show the correctness property of TDPE (i.e., TDPE preserves semantics), we further define a logical relation between residualizing and standard semantics, following Filinski. The use of parametric higher-order abstract syntax (PHOAS) leads to a simple formalization without being disturbed by fresh names created during TDPE. Because of the higher-order nature of PHOAS, it also requires us to prove manually a core property that corresponds to the main lemma of logical relations, which appears to be difficult to prove in Coq.