一句话：在效应处理器语境下提出通用效应契约系统，并证明契约不会不当干扰程序执行。
软件契约让程序员描述组件的行为性质，但现有工作对如何约束效应缺乏通用原则，往往只能为不同效应给出一次性方案。本文在效应处理器（effect handlers）的语境中提出带效应的契约系统设计，使契约能够规约并检查程序的计算效应。其核心元定理表明，契约不会不当地干扰被监控程序的执行。作者实现了该设计，并通过评估展示其通用性，说明该理论足以指导实践。
Software contracts empower programmers to describe functional properties of components. When it comes to constraining effects, though, the literature offers only one-off solutions for various effects. It lacks a universal principle. This paper presents the design of an effectful contract system in the context of effect handlers. A key metatheorem shows that contracts cannot unduly interfere with a program’s execution. An implementation of this design, along with an evaluation of its generality, demonstrates that the theory can guide practice.