一句话：提出 scoped resumptions 限制与证据翻译，证明其可靠一致并实现高效效应处理器。
代数效应处理器能灵活表达效应，但通用形式过于强大，难以推理且实现开销高。本文将处理器限制为具有作用域恢复（scoped resumptions）的子集，论证仍可表达重要效应并改善推理。基于该保证，提出一种可靠且一致的证据翻译：将处理器作为证据直接传给每个操作，并证明到普通 λ 演算的完全可靠性（soundness）与一致性（coherence）。该翻译支持高效实现：尾恢复操作可就地执行而无需捕获求值上下文，并用常量偏移索引替代运行时处理器搜索。
Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.
@article{XieBHSL20,
title = {Effect handlers, evidently},
author = {Ningning Xie and Jonathan Immanuel Brachthäuser and Daniel Hillerström and Philipp Schuster and Daan Leijen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3408981}
}