A Minimal Formulation of Session Types


We study a minimal formulation of session types without sequencing. We show how to forgoing sequencing in types, and only with sequencing on the level of processes, we can recover the usual theory of session types. More specifically, we show an encoding of regular session types into minimal session types, grounded in Parrow’s decomposition of a pi-calculus process into a collection of trios. We show that the correctness of the decomposition using a form of a session-typed bisimulation.

A Minimal Formulation of Session Types (in submission)