一句话：证明有限无递归的 ML 风格语言中一阶引用与续延程序的情境等价可判定，并归约为嵌套数据自动机等价。
本文研究同时含有一般引用（状态）和续延（控制）的 ML 风格语言中的上下文等价问题。作者在有限设定下——基类型有限且无递归——证明：对具有一阶引用与续延、且接口不含续延和引用的程序，上下文等价是可判定的；若允许对函数、续延或引用本身取引用，则该问题不可判定，因此该结果在此设定下已是最优。与以往工作不同，本文不对类型论阶数或项内部一阶引用的使用施加限制，程序甚至可以生成无界堆。判定方法将项的完全抽象迹语义重新表述为具有可判定等价问题的自动机实例，所用自动机属于无限字母表上的数据自动机，其中无限数据集呈森林结构。
We consider contextual equivalence in an ML-like language, where contexts have access to both general references and continuations. We show that in a finitary setting, i.e. when the base types are finite and there is no recursion, the problem is decidable for all programs with first-order references and continuations, assuming they have continuation- and reference-free interfaces. This is the best one can hope for in this case, because the addition of references to functions, to continuations or to references makes the problem undecidable. The result is notable since, unlike earlier work in the area, we need not impose any restrictions on type-theoretic order or the use of first-order references inside terms. In particular, the programs concerned can generate unbounded heaps. Our decidability argument relies on recasting the corresponding fully abstract trace semantics of terms as instances of automata with a decidable equivalence problem. The automata used for this purpose belong to the family of automata over infinite alphabets (aka data automata), where the infinite alphabet (dataset) has the shape of a forest.