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

TL;DR

This paper extends the concept of minimal session types (MSTs) to the session pi-calculus, demonstrating that processes can be simplified to MSTs while preserving correctness, thus providing a foundational understanding of session-based concurrency.

Contribution

It adapts the minimality result of MSTs from higher-order to first-order session pi-calculus and introduces optimizations ensuring dynamic correctness of the process transformations.

Findings

Minimality result for MSTs in session pi-calculus established

Transformations into MSTs are dynamically correct

Optimizations improve process simplification and verification

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.