一句话：提出聚焦多态 CBPV 演算，证明计算完备性，并用聚焦语境建立上下文等价与完全抽象。
聚焦是证明论中利用类型信息剪除证明搜索非必要非确定性的技术；经 Curry-Howard 对应，聚焦推导对应正规形式的项。本文研究如何用聚焦推理上下文等价与完全抽象。作者提出聚焦的多态 call-by-push-value（CBPV）演算，证明计算完备性：每个良类型项都存在 βη 等价的聚焦项。该结果精化了建立上下文等价所需的情境引理，只须考虑聚焦语境。文章展示了聚焦在程序等价（含自由定理）证明中的应用，并证明纯全 CBPV 到带发散与简单效应类型语言的翻译是完全抽象的，给出一个陈述简单但此前难解问题的新解法。
Focusing is a technique from proof theory that exploits type information to prune inessential nondeterminism from proof search procedures. Viewed through the lens of the Curry-Howard correspondence, a focused typing derivation yields terms in normal form. This paper explores how to exploit focusing for reasoning about contextual equivalences and full abstraction. We present a focused polymorphic call-by-push-value calculus and prove a computational completeness result: for every well-typed term, there exists a focused term that is βη-equivalent to it. This completeness result yields a powerful way to refine the context lemmas for establishing contextual equivalences, cutting down the set that must be considered to just focused contexts. The paper demonstrates the application of focusing to establish program equivalences, including free theorems. It also uses focusing to prove full abstraction of a translation of the pure, total call-by-push-value language into a language with divergence and simple effect types, yielding a novel solution to a simple-to-state, but hitherto difficult to solve problem.