AI 中文总结
本文提出基于效应处理程序构建可扩展程序逻辑的方法，从表达性程序逻辑出发，实现模拟多种行为的处理程序并证明其属性以扩展逻辑，还开发关系逻辑，该方法能产生更强推理规则且可扩展。
AI 中文摘要
一种用于推理具有特定类型效应的程序的策略是使用为这些效应的推理提供专门规则的程序逻辑。然而，开发程序逻辑所需的技能与使用程序逻辑所需的技能不同，这使得新逻辑的开发具有挑战性且难以实现。此外，在开发新逻辑时，很难重用先前逻辑中的组件或结合对不同效应的支持。在本文中，我们提出了一种基于效应处理程序在操作上构建可扩展程序逻辑的方法。我们从一种用于推理用纯顺序语言编写的程序并支持效应处理程序的表达性程序逻辑开始。在这种语言中，我们实现了模拟并发、分布式执行和崩溃恢复行为的处理程序。然后，通过证明关于这些处理程序的属性，我们扩展了程序逻辑并导出了用于推理这些效应的表达性规则。在某些情况下，这种方法会产生比针对这些功能的先前程序逻辑中发现的更强的推理规则。此外，我们开发了一种关系逻辑，用于证明使用效应的程序之间的上下文精化。与一元推理一样，处理程序使这种关系逻辑能够以可扩展的方式开发。
英文摘要
One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, developing program logics requires skills that are distinct from those needed for using program logics, making the development of new logics challenging and less accessible. Moreover, when developing new logics, it can be difficult to reuse components from prior logics or combine support for different effects. In this paper, we propose an approach for operationally building extensible program logics based on effect handlers. Our starting point is an expressive program logic for reasoning about programs written in a pure, sequential language with support for effect handlers. Within this language, we implement handlers that model concurrency, distributed execution, and crash-recovery behavior. Then, by proving properties about these handlers, we extend the program logic and derive expressive rules for reasoning about these effects. In some cases, this approach leads to stronger reasoning rules than those found in prior program logics targeting these features. In addition, we develop a relational logic for proving contextual refinements between programs using effects. As with unary reasoning, handlers enable this relational logic to be developed in an extensible way.
