Minimal Session Types for the pi-calculus


Session types enable the static verification of message-passing programs. A session type specifies a channel’s protocol as sequences of messages. Prior work established a minimality result: every process typable with standard session types can be compiled down to a process typable using minimal session types: session types without sequencing construct. This result justifies session types in terms of themselves; it holds for a higher-order session 𝜋-calculus, where values are abstractions (functions from names to processes). This paper establishes a minimality result but now for the session 𝜋-calculus, the language in which values are names and for which session types have been more widely studied. This new minimality result for the session 𝜋 -calculus can be obtained by composing exist- ing results. We develop associated optimizations and enhancements of this result, and establish its static and dynamic correctness.

Minimal Session Types for the pi-calculus (PPDP 2021)