Minimal Session Types for the $π$-calculus (Extended Version)

Session types are a discipline for the static verification of message-passing programs. A session type specifies a channel's protocol as sequences of exchanges. It is most relevant to investigate session-based concurrency by identifying the essential notions that enable program specification and verification. Following that perspective, prior work identified minimal session types (MSTs), a sub-class of session types without the sequentiality construct (;), which specifies the structure of communication actions. This notion led to establish a minimality result: every process typable with standard session types can be compiled down to a process typable using MSTs, which mimics sequentiality in types via additional synchronizations. Such a minimality result is significant because it justifies session types in terms of themselves, without resorting to external notions; it was proven for a higher-order session $\pi$-calculus, where values are abstractions (functions from names to processes). This paper studies MSTs and their associated minimality result 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 this new minimality result can be obtained by composing known results. Then, we develop optimizations of this new minimality result and prove that the associated transformation into processes with MSTs satisfies dynamic correctness.