Skip to Main content Skip to Navigation
Journal articles

A Separation Logic for Effect Handlers

Abstract : User-defined effects and effect handlers are advertised and advocated as a relatively easy-to-understand and modular approach to delimited control. They offer the ability of suspending and resuming a computation and allow information to be transmitted both ways between the computation, which requests a certain service, and the handler, which provides this service. Yet, a key question remains, to this day, largely unanswered: how does one modularly specify and verify programs in the presence of both user-defined effect handlers and primitive effects, such as heap-allocated mutable state? We answer this question by presenting a Separation Logic with built-in support for effect handlers, both shallow and deep. The specification of a program fragment includes a protocol that describes the effects that the program may perform as well as the replies that it can expect to receive. The logic allows local reasoning via a frame rule and a bind rule. It is based on Iris and inherits all of its advanced features, including support for higher-order functions, user-defined ghost state, and invariants. We illustrate its power via several case studies, including (1) a generic formulation of control inversion, which turns a producer that "pushes" elements towards a consumer into a producer from which one can "pull" elements on demand, and (2) a simple system for cooperative concurrency, where several threads execute concurrently, can spawn new threads, and communicate via promises.
Document type :
Journal articles
Complete list of metadata
Contributor : François Pottier Connect in order to contact the contributor
Submitted on : Thursday, December 10, 2020 - 11:07:29 AM
Last modification on : Friday, January 21, 2022 - 3:17:28 AM
Long-term archiving on: : Thursday, March 11, 2021 - 6:34:42 PM


Publisher files allowed on an open archive





Paulo Emílio de Vilhena, François Pottier. A Separation Logic for Effect Handlers. Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (POPL), ⟨10.1145/3434314⟩. ⟨hal-03049514⟩



Les métriques sont temporairement indisponibles