一句话：为一般（含无穷）代数效应建立基于交互树与单子代数的 CBPV 充分性定理。
本文重新探讨代数效应的充分性（adequacy）定理，并将结果推广到包含无穷效应的一般代数效应类。所考虑的演算是 Call-by-Push-Value（CBPV）的一个版本，因此可覆盖包括按值调用在内的多种求值机制。作者为该演算给出基于交互树（interaction trees）的操作语义，以及基于单子代数（monad algebras）的指称语义。核心结果是指称等价蕴含观察等价，即建立充分性；证明采用传统的逻辑关系（logical relations）论证。该工作为不同求值策略下的代数效应语义提供统一框架。
This paper proves an adequacy theorem for a general class of algebraic effects, including infinitary ones. The theorem targets a version of Call-by-Push-Value (CBPV), so that it applies to many possible evaluation mechanisms, including call-by-value. The calculus is given an operational semantics based on interaction trees, as well as a denotational semantics based on monad algebras. The main result, viz. that denotational equivalence implies observational equivalence, using a traditional logical relations argument.