Recursive Session Types Revisited

TL;DR

This paper revisits recursive session types, providing an encoding into recursive linear pi-calculus, and introduces a novel approach to duality in the presence of recursive types, extending previous work on session types and pi-calculus.

Contribution

It presents a new encoding of recursive session types into recursive linear pi-calculus with an improved treatment of duality, building on prior encodings of session types.

Findings

Encoding preserves previous results from non-recursive session types

Introduces a new approach to duality with recursive types

Extends the theoretical framework of session types

Abstract

Session types model structured communication-based programming. In particular, binary session types for the pi-calculus describe communication between exactly two participants in a distributed scenario. Adding sessions to the pi-calculus means augmenting it with type and term constructs. In a previous paper, we tried to understand to which extent the session constructs are more complex and expressive than the standard pi-calculus constructs. Thus, we presented an encoding of binary session pi-calculus to the standard typed pi-calculus by adopting linear and variant types and the continuation-passing principle. In the present paper, we focus on recursive session types and we present an encoding into recursive linear pi-calculus. This encoding is a conservative extension of the former in that it preserves the results therein obtained. Most importantly, it adopts a new treatment of the duality relation, which in the presence of recursive types has been proven to be quite challenging.