Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

This paper considers the challenge of establishing the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. We present Asynchronous Priority-based Classical Processes (APCP), a typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. APCP builds upon the Curry-Howard correspondences between linear logic and session types; using these foundations, we establish the essential meta-theoretical results of APCP, in particular deadlock-freedom. To illustrate the expressiveness of APCP, we formulate and study CGV, a new concurrent $\lambda$-calculus with asynchronous sessions. We establish the correct encodability of asynchronous terms in CGV into asynchronous processes in APCP.