Recursive Session Types Revisited
Open Access
- 24 August 2014
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 162, 27-34
- https://doi.org/10.4204/eptcs.162.4
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.Comment: In Proceedings BEAT 2014, arXiv:1408.556This publication has 7 references indexed in Scilit:
- Session types revisitedPublished by Association for Computing Machinery (ACM) ,2012
- Fundamentals of session typesInformation and Computation, 2012
- Bounded polymorphism in session typesMathematical Structures in Computer Science, 2008
- Subtyping for session types in the pi calculusActa Informatica, 2005
- Linearity and the pi-calculusACM Transactions on Programming Languages and Systems, 1999
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- An interaction-based language and its typing systemLecture Notes in Computer Science, 1994