一句话：提出线性并发分离逻辑 LinearActris，用线性性保证依赖高阶消息传递程序无死锁且无泄漏。
本文面向消息传递并发，研究如何静态保证程序无死锁与无资源泄漏。作者提出线性并发分离逻辑 LinearActris，融合会话类型与并发分离逻辑，支持通过依赖协议验证带可变状态的高阶程序。核心难点是证明该逻辑的 adequacy 定理，即线性性确实“免费”带来无死锁与无泄漏；作者基于连通图（connectivity graphs）定义步进索引的分离逻辑模型来完成证明。为展示表达能力，他们利用逻辑关系证明了高阶 GV 风格会话类型系统的可靠性。所有结果与示例均在 Coq 中机械化。
We introduce a linear concurrent separation logic, called LinearActris , designed to guarantee deadlock and leak freedom for message-passing concurrency. LinearActris combines the strengths of session types and concurrent separation logic, allowing for the verification of challenging higher-order programs with mutable state through dependent protocols. The key challenge is to prove the adequacy theorem of LinearActris, which says that the logic indeed gives deadlock and leak freedom “for free” from linearity. We prove this theorem by defining a step-indexed model of separation logic, based on connectivity graphs . To demonstrate the expressive power of LinearActris, we prove soundness of a higher-order (GV-style) session type system using the technique of logical relations. All our results and examples have been mechanized in Coq.
@article{paperbot2616,
title = {Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing},
author = {Jules Jacobs and Jonas Kastberg Hinrichsen and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632889}
}