一句话:揭示并发分离逻辑与差分线性逻辑模板博弈语义的范畴联系,并据此重构 CSL 的异步交互解释。
并发理论与程序语言语义一直试图揭示调节高阶程序博弈语义与共享内存和锁的并发程序 Hoare 逻辑的基本同步机制。本文在并发分离逻辑(CSL)与差分线性逻辑(DiLL)的模板博弈语义这两个近期研究方向之间建立了一个深刻而意想不到的联系。借助这一联系,作者用 DiLL 模板博弈的纯概念风格,重新表述了 Melliès 和 Stefanesco 此前为 CSL 设计的异步交互解释。该分析被认为揭示了 CSL 的隐秘结构,特别是顺序组合、并行积、错误与锁之间具有范畴性质的微妙交互。
An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. We establish a deep and unexpected connection between two recent lines of work on concurrent separation logic (CSL) and on template game semantics for differential linear logic (DiLL). Thanks to this connection, we reformulate in the purely conceptual style of template games for DiLL the asynchronous and interactive interpretation of CSL designed by Melliès and Stefanesco in a recent work. We believe that the analysis reveals something important about the secret anatomy of CSL, and more specifically about the subtle interplay, of a categorical nature, between sequential composition, parallel product, errors and locks.