2014/08/26 by Ornela Dardha
Computer Science · #cs.PL
paper · pdf · doi:10.4204/eptcs.162.4
published as EPTCS 162, 2014, pp. 27-34 · In Proceedings BEAT 2014, arXiv:1408.5564
arxiv created 2014/08/26 · arxiv updated 2014/08/27
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.