EXPRESSing Session Types

TL;DR

This paper presents an encoding of session types within a type theory for the π-calculus, enabling better analysis, inference, and understanding of session-based communication protocols.

Contribution

It introduces a novel encoding that leverages π-calculus results for session types, enhancing deadlock analysis and type inference capabilities.

Findings

Enables refined deadlock analysis for session types

Allows session type inference using standard type inference algorithms

Deepens theoretical understanding of session types through π-calculus encoding

Abstract

To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $\pi$-calculus by means of a suitable encoding. The encoding allows one to reuse results about the $\pi$-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical foundations. Perhaps surprisingly, the encoding has practical implications as well, by enabling refined forms of deadlock analysis as well as allowing session type inference by means of a conventional type inference algorithm.