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

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 \pi-calculus, where values are abstractions (functions from names to processes). This paper establishes a minimality result but now for the session \pi-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 \pi-calculus can be obtained by composing existing results. We develop associated optimizations of this result, and establish its static and dynamic correctness.