一句话：提出首个面向 effect handlers 的关系分离逻辑 blaze，支持在含可变状态与并发的程序中证明程序间关系性质。
Effect handlers 可简洁控制执行流，但现有验证工具无法在 OCaml、Links 等含可变状态与并发的语言中证明程序间关系性质。本文提出 blaze，首个面向 effect handlers 的关系分离逻辑，构建于 Rocq 的并发分离逻辑框架 Iris 之上，继承机器化理论与模块化并发推理、自定义 ghost state 能力。blaze 提供 bind、frame 等规则，支持对 perform/handle 的模块化推理，且验证两程序关系时不要求双方 effect 与 handler 对应。通过多个案例研究，作者将基于 effects 的异步编程库实现与真正并发实现关联起来，并给出独立于 effects 的 logical-fork 与 thread-swap 规则。
Effect handlers offer a powerful and relatively simple mechanism for controlling a program’s flow of execution. Since their introduction, an impressive array of verification tools for effect handlers has been developed. However, to this day, no framework can express and prove relational properties about programs that use effect handlers in languages such as OCaml and Links, where programming features like mutable state and concurrency are readily available. To this end, we introduce blaze , the first relational separation logic for effect handlers. We build blaze on top of the Iris framework for concurrent separation logic in Rocq, thereby enjoying the rigour of a mechanised theory and all the reasoning properties of a modern fully-fledged concurrent separation logic, such as modular reasoning about stateful concurrent programs and the ability to introduce user-defined ghost state. In addition to familiar reasoning rules, such as the bind rule and the frame rule, blaze offers rules to reason modularly about programs that perform and handle effects. Significantly, when verifying that two programs are related, blaze does not require that effects and handlers from one program be in correspondence with effects and handlers from the other. To assess this flexibility, we conduct a number of case studies: most noticeably, we show how different implementations of an asynchronous-programming library using effects are related to truly concurrent implementations. As side contributions, we introduce two new, simple, and general reasoning rules for concurrent relational separation logic that are independent of effects: a logical-fork rule that allows one to reason about an arbitrary program phrase as if it had been spawned as a thread and a thread-swap rule that allows one to reason about how threads are scheduled.
@article{VilhenaCWK26,
title = {A Relational Separation Logic for Effect Handlers},
author = {Paulo Emílio de Vilhena and Simcha van Collem and Ines Wright and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776676}
}