Recursive Session Types Revisited

Ornela Dardha
(School of Computing Science, University of Glasgow)

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.

In Marco Carbone: Proceedings Third Workshop on Behavioural Types (BEAT 2014), Rome, Italy, 1st September 2014, Electronic Proceedings in Theoretical Computer Science 162, pp. 27–34.
Published: 24th August 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: