一句话：将共享可变状态融入会话并发语言的命题即类型线性逻辑解释，并保持安全与活性。
本文研究如何将共享可变状态原则性地集成到基于会话的并发编程语言的命题即类型（propositions-as-types）线性逻辑解释中。传统上，函数核心的类型系统常基于命题即类型对应自动保证强安全性和活性，而命令式特性多依赖逻辑外构造。作者受微分线性逻辑规则启发，将非确定性与共享机制纳入逻辑系统，支持可共享的一等引用单元存储任意持久对象。系统保证会话保真、进展、合流与规范化；并证明在自然扩展的一等锁下，保持性和进展仍能成立。文中还通过示例展示其表达能力，包括可共享的并发抽象数据类型。
We develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.