一句话：将带局部整数引用的高阶程序上下文等价归约为内存配置迁移系统的不可达性，并用约束 Horn 子句自动判定。
论文研究带局部整数引用的按值调用函数式语言中程序的上下文等价问题。作者提出一个框架，将该问题归约为内存配置迁移系统中的不可达性；对无递归程序，该归约是完备的。进一步限制函数体内部不分配引用时，可把不可达性编码为一组约束 Horn 子句，并借助求解器自动检查可满足性。若再限制到有限数据类型语言，则得到任意类型下上下文等价的新可判定性结果。该工作为高阶引用程序的上下文等价提供了自动验证途径，并扩展了可判定边界。
We propose a framework to study contextual equivalence of programs written in a call-by-value functional language with local integer references. It reduces the problem of contextual equivalence to the problem of non-reachability in a transition system of memory configurations. This reduction is complete for recursion-free programs. Restricting to programs that do not allocate references inside the body of functions, we encode this non-reachability problem as a set of constrained Horn clause that can then be checked for satisfiability automatically. Restricting furthermore to a language with finite data-types, we also get a new decidability result for contextual equivalence at any type.
@article{paperbot514,
title = {SyTeCi: automating contextual equivalence for higher-order programs with references},
author = {Guilhem Jaber},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371127}
}