Dependent Session Protocols in Separation Logic from First Principles - Functional Pearl

Explore a 28-minute conference talk from ICFP 2023 that delves into developing dependent session protocols in concurrent separation logic for functional languages with message-passing. Learn about a layered design approach inspired by minimalistic session calculi, starting from mutable references and building up to one-shot channels, session channels, and imperative channels. Discover how this approach simplifies the verification of one-shot protocols and enables the definition of dependent session protocols without requiring advanced mechanisms. Understand the advantages of this method in terms of simplicity, elegance, and flexibility, including automatic support for subprotocols and guarded recursion. Gain insights into the meta theory behind these results and learn about the mechanization of all findings using the Iris framework in less than 1000 lines of Coq code. Access the full article and supplementary archive for further exploration of this functional pearl presented by researchers from Radboud University Nijmegen and Aarhus University.