POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 10:20 - 10:45 at Réfectoire - Separation Logic Chair(s): Derek Dreyer

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 Rocq implementation of the Iris separation logic, 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.

Thu 15 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:20 - 12:00
Separation LogicPOPL at Réfectoire
Chair(s): Derek Dreyer MPI-SWS
10:20
25m
Talk
A Relational Separation Logic for Effect Handlers
POPL
Paulo Emílio de Vilhena Imperial College London, Simcha van Collem Radboud University Nijmegen, Ines Wright Aarhus University, Robbert Krebbers Radboud University Nijmegen
DOI
10:45
25m
Talk
Bayesian Separation Logic
POPL
Shing Hin Ho Imperial College London, Nicolas Wu Imperial College London, Azalea Raad Imperial College London
DOI Pre-print
11:10
25m
Talk
Cryptis: Cryptographic Reasoning in Separation Logic
POPL
Arthur Azevedo de Amorim Rochester Institute of Technology, Amal Ahmed Northeastern University, USA, Marco Gaboardi Boston University
DOI
11:35
25m
Talk
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
POPL
Neta Elad Tel Aviv University, Adithya Murali University of Wisconsin, Sharon Shoham Tel Aviv University
DOI