Minimal Session Types for the pi-calculus

Abstract

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 existing results. We develop associated optimizations and enhancements of this result, and establish its static and dynamic correctness.

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

Related