一句话：提出下推正规形式互模拟，可可靠、完备且对调用栈无界情形可判定地验证高阶函数式程序上下文等价。
论文研究带局部状态的高阶函数式语言的上下文等价验证。传统正规形式（NF）互模拟虽可靠且完备，但对可增长到无界配置的程序项不可判定。作者提出下推正规形式（PDNF）互模拟，其核心思想是：当无界性来自调用栈时，可用接受初始/最终栈内容的有限状态自动机模拟下推系统。为此构造无栈标签迁移系统（LTS），并引入调用栈的即时饱和过程，在该系统上定义互模拟，同时发展 up-to 技术。论文证明 PDNF 互模拟相对上下文等价既可靠又完备，并对一类栈无界程序项可判定。原型实现能验证文献中的等价性以及受真实代码启发的、此前方法无法处理的例子。
We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that can reach configurations of unbounded size, so long as the source of unboundedness is the call stack. Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content. We embody this in a stack-less Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined. We develop up-to techniques and a prototype implementation able to verify equivalences from the literature and others inspired by real code, which were out of reach for previous work.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{KoutavasLT24,
title = {Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence},
author = {Vasileios Koutavas and Yu-Yang Lin and Nikos Tzevelekos},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662103}
}