Asynchronous Functional Sessions: Cyclic and Concurrent (Extended Version)

TL;DR

This paper introduces Concurrent GV (CGV), a session-typed calculus supporting asynchronous message-passing with enhanced concurrency and cyclic topologies, building on APCP to ensure deadlock freedom.

Contribution

It develops the syntax, semantics, and type system for CGV, and provides a translation to APCP along with deadlock-freedom techniques.

Findings

CGV supports cyclic and concurrent network topologies.

A correct translation from CGV to APCP is established.

Deadlock freedom is achieved using APCP's priority-based type system.

Abstract

We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system.