一句话：将共享机制引入会话类型语言，通过线性/共享分层与模态算子，在保持会话保真性的同时允许共享进程竞争导致的死锁。
基于线性逻辑与会话类型通信的 Curry-Howard 对应，会话类型语言可保证会话保真性与无死锁，但这些强保证排除了许多共享资源的自然编程模式。本文在会话类型语言中引入共享：类型被分层为线性层与共享层，并通过模态算子连接两层。所得语言保持会话保真性，但不再保证无死锁，因为对共享进程的竞争可能引发死锁。作者用哲学家就餐等例子说明该语言，并给出无类型异步 π 演算到该语言的翻译。
Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this paper, we introduce sharing into a session-typed language where types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. We illustrate our language on various examples, such as the dining philosophers problem, and provide a translation of the untyped asynchronous π-calculus into our language.