一句话：提出异构双正交步进索引逻辑关系，证明效应子类型下强制语义的一致性，并机器化验证选择性 CPS 翻译。
带子类型的编程语言的强制（coercion）语义通常定义在类型推导而非类型判断上，因此必须保证一致性：同一判断的不同推导得到相同语义。本文提出异构、双正交、步进索引的逻辑关系，用于证明这类强制语义的一致性。为展示方法有效性，作者研究带定界续延与控制效应子类型的按值调用 lambda 演算，给出类型导向的选择性 CPS 翻译，并用该逻辑关系证明其强制语义一致。文章还包含 Coq 形式化，依赖一种用于步进索引推理的新型浅嵌入逻辑。
A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherence of coercion semantics of programming languages with subtyping. To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. The article is accompanied by a Coq formalization that relies on a novel shallow embedding of a logic for reasoning about step-indexing.