一句话：在带代数效应的 call-by-value λ-演算中，用 monad 和 relator 抽象推广应用性互模拟，并刻画其成为同余的条件。
论文研究带代数效应的 call-by-value λ-演算中的程序等价性。作者首先为计算 λ-演算配备 monadic 操作语义，将代数效应封装在 monad 中；随后引入 relator 理论，把 Abramsky 的应用性互模拟从纯演算抽象地推广到该设定。核心问题是：对于哪些 monad 与 relator，应用性互模拟仍是同余关系，从而可作为可靠的程序等价方法。为此，论文在抽象层面研究 Howe 方法，并给出保证同余性的条件。该工作提供了一个统一语义框架，使应用性互模拟可适用于多种效应与等价概念，并为带效应语言的共归纳等价证明奠定方法论基础。
We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value λ-calculi with algebraic effects. We first of all endow a computational λ-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract.