一句话：用最基础的并发分离逻辑机制分层构造依赖会话协议，并在 Iris/Coq 中机器化验证。
本文在带消息传递的函数式语言的并发分离逻辑中，给出依赖会话协议的一种构造性处理。此前工作验证依赖会话协议时，需要递归域方程和高阶幽灵状态等高级机制。本文受极简会话演算启发，采用分层设计：从可变引用出发，依次构造一次性通道、会话通道和命令式通道。核心思路是仅使用最基本的机制验证一次性通道满足一次性协议，随后把该规范当作黑盒，在其上定义依赖会话协议。这种分层带来简洁性、优雅性与灵活性：子协议和守卫递归的支持自动从一次性协议转移至依赖会话协议，并可轻松获得多种通道关闭形式。由于元理论简单，论文给出了全部定义，并在 Iris 框架中用不到 1000 行 Coq 机器化了所有结果。
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.
@article{paperbot1905,
title = {Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)},
author = {Jules Jacobs and Jonas Kastberg Hinrichsen and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607856}
}