一句话：提出首个针对按值调用 PCF 的完全抽象正规形式双模拟，并实现有界检查工具。
论文为按值调用 PCF（PCFv）提出首个完全抽象的正规形式双模拟。问题在于获得既可靠又完备、且无需语义商化的程序等价证明方法。方法上，作者构建了一个标记迁移系统（LTS），融合应用双模拟、环境双模拟与博弈语义；该 LTS 生成与可能函数上下文交互对应的轨迹，从而在避免语义商化的同时获得完备性。由此得到检查 PCFv 程序等价的可靠且完备技术，并实现有界双模拟检查工具。评估方面，作者在文献中已知的等价实例和新例子上测试了该工具。
We present the first fully abstract normal form bisimulation for call-by-value PCF (PCFv). Our model is based on a labelled transition system (LTS) that combines elements from applicative bisimulation, environmental bisimulation and game semantics. In order to obtain completeness while avoiding the use of semantic quotiening, the LTS constructs traces corresponding to interactions with possible functional contexts. The model gives rise to a sound and complete technique for checking of PCFv program equivalence, which we implement in a bounded bisimulation checking tool. We test our tool on known equivalences from the literature and new examples.