一句话：提出支持循环网络异步通信的会话类型框架 APCP 与并发 λ 演算 LASTn，并保证无死锁。
本文研究循环进程网络中异步消息传递进程的无死锁保证。作者提出 APCP，一种基于会话类型的进程框架，支持异步通信、委托与递归；借助线性逻辑与会话类型之间的 Curry-Howard 对应，建立其元理论结果，尤其是无死锁性。随后提出带异步会话类型的并发 λ 演算 LASTn，给出示例并建立其元理论结果。为将 APCP 的无死锁保证可靠迁移至 LASTn，作者发展从 LASTn 项到 APCP 进程的翻译，并证明其满足强操作对应。该工作为异步循环会话并发提供统一类型化基础。
We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $\lambda$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence.
@article{paperbot2719,
title = {Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks},
author = {Bas van den Heuvel and Jorge A. Pérez},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:6)2024}
}