paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Concurrent Separation Logic Meets Template Games

并发分离逻辑遇上模板博弈
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 该论文属于并发分离逻辑与差分线性逻辑模板博弈语义的纯范畴论/形式语义研究,虽处在 PL 与形式化方法的大领域内,但与用户关注的四个核心问题(PL→AI 静态分析、AI→PL 验证、浮点程序分析、贝叶斯程序分析)均无直接交集,也不涉及 LLM/Agent 或工业落地。引用 1 inbox
Paul-André Melliès, Léo Stefanesco
crossref: 2026-09-12

AI 速览

一句话:揭示并发分离逻辑与差分线性逻辑模板博弈语义的范畴联系,并据此重构 CSL 的异步交互解释。

并发理论与程序语言语义一直试图揭示调节高阶程序博弈语义与共享内存和锁的并发程序 Hoare 逻辑的基本同步机制。本文在并发分离逻辑(CSL)与差分线性逻辑(DiLL)的模板博弈语义这两个近期研究方向之间建立了一个深刻而意想不到的联系。借助这一联系,作者用 DiLL 模板博弈的纯概念风格,重新表述了 Melliès 和 Stefanesco 此前为 CSL 设计的异步交互解释。该分析被认为揭示了 CSL 的隐秘结构,特别是顺序组合、并行积、错误与锁之间具有范畴性质的微妙交互。

问题
研究问题:如何揭示并发分离逻辑中共享内存与锁的同步机制,并将其与高阶程序博弈语义及线性逻辑置于统一的语义视角下理解。
方法
方法:建立 CSL 与 DiLL 模板博弈语义之间的深层范畴联系,并用模板博弈的风格重构 CSL 的异步交互解释。
评估
评估:属于理论/概念性工作,通过语义对应与重构论证两种框架之间的联系,摘要未报告实验评估。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot5482,
  title = {Concurrent Separation Logic Meets Template Games},
  author = {Paul-André Melliès and Léo Stefanesco},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394762}
}