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}
}