On the Expressiveness of Asynchronous Processes with Nested Session Types

Overview & Synopsis

Session types are a type-based approach to correct message-passing programs, where types specify protocols for channels and type checking guarantees communication correctness. Traditional session types express regular protocols only, which leaves out many protocols found in practice. Aiming at overcoming this limitation, Nested Session Types (NSTs) can specify nested recursive protocols. NSTs are known to be characterised by one-counter machines and deterministic context-free languages. In this paper, we study the expressiveness of ASP (Asynchronous Session Processes), the process model associated with NSTs as introduced by Das et al. We prove that AST is Turing complete by giving a correct encoding of two-counter machines into typed processes. Our encoding uses a non-trivial state-aware representation of counters and instructions that is neatly governed by NSTs.