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 π-calculus, in which values are abstractions (functions from names to processes). In this paper, we study MSTs but now for the session π-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.