一句话：提出异步代数效应核心演算 λæ，将操作调用解耦为信号与结果中断，并给出类型安全证明与原型。
论文研究如何用代数效应支持异步编程。传统代数效应通常同步处理操作调用，本文将其扩展为异步：调用操作时只发出需要执行实现的信号，运行中的计算可继续执行，随后被该操作的结果中断，并通过安装中断处理器对结果作出反应。作者在小型核心演算 λæ 中形式化该机制，在 Agda 中机器化验证其类型安全，并给出 OCaml 原型实现。案例研究涵盖多方 Web 应用、抢占式多线程、远程函数调用以及代数效应 runner 的并行变体，展示了该设计在异步场景中的表达力与灵活性。
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, called λ æ . We demonstrate the flexibility of λ æ using examples ranging from a multi-party web application, to preemptive multi-threading, to remote function calls, to a parallel variant of runners of algebraic effects. In addition, the paper is accompanied by a formalisation of λ æ ’s type safety proofs in Agda, and a prototype implementation of λ æ in OCaml.