一句话：提出 Affect：用仿射类型与效应静态追踪续延的 one-shot/multi-shot 用法，并在 Coq/Iris 中证明其可靠性。
效应处理器的续延可被恢复一次（one-shot）或任意多次（multi-shot）；multi-shot 会破坏关键推理规则，使某些标准变换与优化不再可靠，在含可变引用的语言（如 OCaml 5）中尤为明显。本文提出 Affect——用仿射类型追踪续延用法的类型与效应系统，使编译器能据此高效实现效应处理器并判定可执行的优化。为支持存储续延的引用、嵌套续延等高级特性，作者扩展了 Rust 的 Cell 类型与 Wadler 的 use types，并支持多态效应函数的一般类型签名。作者在 Coq 的 Iris 分离逻辑中用逻辑关系对类型与判定作语义建模，证明了 Affect 的可靠性。
Effect handlers form a powerful construct that can express complex programming abstractions. They are a generalisation of exception handlers, but allow resumption of the continuation from where the effect was raised. Allowing continuations to be resumed at most once ( one-shot ) or an arbitrary number of times ( multi-shot ) has far-reaching consequences. In addition to performance considerations, multi-shot effects break key rules of reasoning and thus render certain standard transformation/optimisations unsound, especially in languages with mutable references (such as OCaml 5). It is therefore desirable to statically track whether continuations are used in a one-shot or multi-shot discipline, so that a compiler could use this information to efficiently implement effect handlers and to determine what optimizations it may perform. We address this problem by developing a type and effect system–called Affect –which uses affine types to track the usage of continuations. A challenge is to soundly deal with advanced programming features—such as references that store continuations and nested continuations—which are crucial to support challenging examples from the effects literature (such as control inversion and cooperative concurrency ). Another challenge is to support generic type signatures of polymorphic effectful functions. We address these challenges by using and extending Rust's Cell type and Wadler's use types . To prove soundness of Affect we model types and judgements semantically via a logical relation in the Iris separation logic framework in Coq.