Minimal session types for the -calculus

Session types are a type-based approach to correct message-passing programs. A session type specifies a channel's protocol as sequences of exchanges. Aiming to uncover the essential notions of session-based concurrency, prior work defined minimal session types (MSTs), a formulation of session types without the sequentiality construct, and showed a minimality result: every process typable with standard session types can be transformed into a process typable using MSTs. Such a minimality result was proven for a higher-order session pi-calculus, in which values are abstractions (functions from names to processes). In this paper, we study MSTs but now for the session pi-calculus, the (first-order) language in which values are names and for which session types have been more widely studied. We first show that a new minimality result can be obtained by composing known results. Then, we develop optimizations of this new minimality result and prove also a dynamic correctness guarantee. (c) 2024 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).