一句话：提出高阶异步效应，将操作调用解耦为信号与中断，用核心演算统一异步与代数效应。
代数效应通常按同步方式处理，难以自然表达异步计算。本文在高阶代数效应中引入异步机制：将操作调用的执行解耦为“发出需要执行该操作的信号”和“用操作结果中断当前计算”，后者可通过安装中断处理器来响应。作者用一个小型核心演算形式化该思想，并以多方 Web 应用、抢占式多线程、可取消远程函数调用及并行效应 runner 等例子展示其灵活性。类型安全证明已在 Agda 中机器化，并给出 OCaml 原型实现。
We explore asynchronous programming with algebraic effects. We complement their conventional synchronous treatment by showing how to naturally also accommodate asynchrony within them, namely, by decoupling the execution of operation calls into signalling that an operation's implementation needs to be executed, and interrupting a running computation with the operation's result, to which the computation can react by installing interrupt handlers. We formalise these ideas in a small core calculus and demonstrate its flexibility using examples ranging from a multi-party web application, to pre-emptive multi-threading, to (cancellable) remote function calls, to a parallel variant of runners of algebraic effects. In addition, the paper is accompanied by a formalisation of the calculus's type safety proofs in Agda, and a prototype implementation in OCaml.