A Minimal Formulation of Session Types: The Sessions of Trios in Concert

TL;DR

This paper introduces minimal session types, demonstrating that complex sequencing in session types can be replaced by sequencing in processes without losing behavioral correctness, simplifying the theoretical framework.

Contribution

It proves that standard session types can be reduced to minimal session types through compilation, maintaining behavioral equivalence, thus simplifying session type systems.

Findings

Every process typable with standard session types can be compiled into a process with minimal session types.

The compiled process is behaviorally equivalent to the original process.

Minimal session types are supported by static and dynamic correctness results.

Abstract

Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential to enforcing program correctness; by relying on sequencing constructs, a session type can precisely describe the intended order of communication actions through a channel. In this paper we study a fragment of session types that makes a very limited use of sequencing; we call it minimal session types. In the context of a core process calculus with sessions and higher-order concurrency, we establish two technical results. First, we prove that every process P typable with standard session types can be compiled down into a process D(P) typable with minimal session types. Second, we prove that P and D(P) are behaviorally equivalent. These results show that having sequencing in both processes and session types is convenient, but that only sequencing in processes is truly indispensable, as it can correctly codify sequencing in types. Our developments draw inspiration from work by Parrow on behavior-preserving decompositions of untyped processes using trios, i.e., processes with exactly three nested prefixes. By casting Parrow's approach in the realm of typed processes, our developments reveal a conceptually simple formulation of session types, supported by static and dynamic correctness results.