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 metadatas

https://hal.inria.fr/hal-03049514
Contributor : François Pottier <>
Submitted on : Thursday, December 10, 2020 - 11:07:29 AM
Last modification on : Thursday, January 7, 2021 - 3:37:13 AM

File

de-vilhena-pottier-sleh.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

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

Share

Metrics

Record views

33

Files downloads

55