ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Thu 7 Sep 2023 14:00 - 14:30 at A - Grand Ballroom 2 - Session typing functional pearls Chair(s): Andrew K. Hirsch

We develop an account of dependent session protocols in concurrent separation logic for a functional language with message-passing.
Inspired by minimalistic session calculi,
we present a layered design:
starting from mutable references, we build one-shot channels, session channels, and imperative channels.
Whereas previous work on dependent session protocols in concurrent separation logic required advanced mechanisms such as recursive domain equations and higher-order ghost state,
we only require the most basic mechanisms to verify that our one-shot channels satisfy one-shot protocols,
and subsequently treat their specification as a black box on top of which we define dependent session protocols.
This has a number of advantages in terms of simplicity, elegance, and flexibility:
support for subprotocols and guarded recursion automatically transfers from the one-shot protocols to the dependent session protocols,
and we easily obtain various forms of channel closing.
Because the meta theory of our results is so simple,
we are able to give all definitions as part of this paper,
and mechanize all our results using the Iris framework in less than 1000 lines of Coq.

Thu 7 Sep

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:30
Session typing functional pearlsICFP Papers and Events at A - Grand Ballroom 2
Chair(s): Andrew K. Hirsch University at Buffalo, SUNY
Intrinsically Typed Sessions with Callbacks (Functional Pearl)Functional Pearl
ICFP Papers and Events
Peter Thiemann University of Freiburg, Germany
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)Functional PearlRemote
ICFP Papers and Events
Jules Jacobs Radboud University Nijmegen, Jonas Kastberg Hinrichsen Aarhus University, Denmark, Robbert Krebbers Radboud University Nijmegen