Capturing the reasoning principles of undelimited continuations in a separation logic has proven challenging: previous logics for call/cc abandon either the frame rule, the core of separation logic, or the bind rule, the key principle to verify programs by parts. We show that by incorporating a one-shot restriction, namely that the captured continuations can only be used once, both principles can be recovered in a novel Iris-based separation logic for call/1cc and call/1cc0, the construct whose semantics incorporates this restriction. The logic enjoys elegant, relatively simple, but yet powerful principles: we show it is sufficient to conduct sophisticated case studies including call/1cc0-based implementations of control inversion, cooperative concurrency, and effect handlers similar to Filinski's encoding of shift/reset. The latter case study further suggests a notion of context-independent user-defined effects, which implement a functionality regardless of the control stack. Our results are formalized in Rocq using Iris.
[ bib | Local copy ] Back
This file was generated by bibtex2html 1.99.