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.

翻译：会话类型是用于消息传递程序静态验证的一种规范方法。会话类型将通道的协议指定为一系列交换。通过识别实现程序规范与验证的基本概念，研究基于会话的并发性具有重要价值。基于这一视角，先前工作提出了最小会话类型（MSTs）——这是一种不含顺序性构造符（;）的会话类型子类，该构造符用于定义通信动作的结构。该概念引出了一项最小性结论：所有使用标准会话类型可类型化的进程，均可编译为使用MSTs可类型化的进程，后者通过额外同步机制模拟类型中的顺序性。这一最小性结论的重要意义在于，它无需借助外部概念即可用会话类型自身为其提供合理性证明。该结论最初针对高阶会话$π$-演算（其中值为从名称到进程的抽象函数）得以证明。本文研究MSTs及其相关的最小性结论，但首次聚焦于会话$π$-演算——即值域为名称的一阶语言，会话类型在该语言中得到了更广泛的研究。我们首先证明通过组合已知结果可获得这一新的最小性结论，继而开发该结论的优化方案，并证明与其对应的MSTs进程转换满足动态正确性。