[DLY+08] On Progress for Structured Communications

Abstract

We propose a new typing system for the pi-calculus with sessions, which ensures the progress property, i.e. once a session has been initiated, typable processes will never starve at session channels. In the current literature progress for session types has been guaranteed only in the case of nested sessions, disallowing more than two session channels interfered in a single thread. This was a severe restriction since many structured communications need combinations of sessions. We overcome this restriction by inferring the order of channel usage, but avoiding any tagging of channels and names, neither explicit nor inferred. The simplicity of the typing system essentially relies on the session typing discipline, where sequencing and branching of communications are already structured by types. The resulting typing enjoys a stronger progress property than that one in the literature: it assures that for each well typed process P which contains an open session there is a well typed and irreducible process Q such that the parallel composition P¦Q always reduces, also in presence of interfered sessions.

@inproceedings{DLY07, volume = 4912, pdf = {http://www.di.unito.it/~dezani/papers/dlyshort.pdf}, author = {Dezani-Ciancaglini, Mariangiola and de' Liguoro, Ugo and Yoshida, Nobuko}, series = {LNCS}, booktitle = {TGC'07}, editor = {Gilles Barthe and C\'edric Fournet}, abstract = {We propose a new typing system for the pi-calculus with sessions, which ensures the progress property, i.e. once a session has been initiated, typable processes will never starve at session channels. In the current literature progress for session types has been guaranteed only in the case of nested sessions, disallowing more than two session channels interfered in a single thread. This was a severe restriction since many structured communications need combinations of sessions. We overcome this restriction by inferring the order of channel usage, but avoiding any tagging of channels and names, neither explicit nor inferred. The simplicity of the typing system essentially relies on the session typing discipline, where sequencing and branching of communications are already structured by types. The resulting typing enjoys a stronger progress property than that one in the literature: it assures that for each well typed process P which contains an open session there is a well typed and irreducible process Q such that the parallel composition P|Q always reduces, also in presence of interfered sessions.}, tag = {{TGC'07}}, title = {{On Progress for Structured Communications}}, publisher = {Springer}, year = {2008}, pages = {257--275}, }

DLY07 (In proceedings)
Author(s)	Mariangiola Dezani-Ciancaglini, Ugo de' Liguoro and Nobuko Yoshida
Title	« On Progress for Structured Communications »
In	TGC'07
Series	LNCS
Editor(s)	Gilles Barthe and Cédric Fournet
Volume	4912
Page(s)	257--275
Year	2008
Publisher	Springer
PDF	http://www.di.unito.it/˜dezani/papers/dlyshort.pdf