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

TL;DR

The paper advances MST theory by providing two distinct decompositions that translate standard session-typed π-calculus processes into MST-typed processes. The first, a decompose-by-composing approach, leverages existing encodings between $ extsf{HO}$ and $ ext{π}$ to lift MST minimality from higher-order settings to the π-calculus; the second, an optimized $ ext{F}^*$-based decomposition, reduces redundant synchronizations and directly handles recursion and recursive types. It proves static correctness for both decompositions and establishes dynamic correctness for the optimized variant via MST-bisimilarity, demonstrating that the π-process and its MST-based counterpart are behaviorally equivalent. Together, these results show that sequentiality in session types is not essential to verification: MSTs suffice to capture the core structure of communications, even in first-order, recursive, and higher-order-embedded settings, bridging first- and higher-order session theories. This work thus deepens understanding of session-based concurrency and offers practical decompositions for implementing MSTs in π-calculus-like languages.

Abstract

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 formulation of session types 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 process 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, in which values are abstractions (functions from names to processes). In this paper, we study 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.

Figures (5)

• Figure 1: First approach to a minimality result for $\pi$: Decompose by Composing.
• Figure 2: Syntax of $\mathsf{HO}\pi$. The calculus $\pi$ is the sub-language of $\mathsf{HO}\pi$ that lacks $\text{boxed}$ constructs, whereas $\mathsf{HO}$ is the sub-language that lacks $\text{shaded}$ constructs.
• Figure 3: Reduction Semantics of $\mathsf{HO}\pi\xspace$.
• Figure 4: The Untyped LTS for $\mathsf{HO}\pi$ processes. We omit Rule ${\footnotesize \langle \textsc{Par${}_R$} \rangle}$.
• Figure 5: STs for $\mathsf{HO}\pi$ (top) and MSTs for $\mathsf{HO}$ (bottom).