| Abstract |
| We define session types as projections of the behavior of processes with respect to the operations processes perform on channels. This calls for a parallel composition operator over session types denoting the simultaneous access to a channel by two or more processes. The proposed approach allows us to define a semantically grounded theory of session types that does not require the linear usage of channels. However, type preservation and progress can only be guaranteed for processes that never receive channels they already own. A number of examples show that the resulting framework validates existing session type theories and unifies them to some extent. |
@article{Padovani12,
volume = {22},
issn = {0960-1295},
author = {Luca Padovani},
issue = {2},
url = {http://www.di.unito.it/~padovani/Papers/projection.pdf},
abstract = { We define session types as projections of the behavior of
processes with respect to the operations processes perform on
channels. This calls for a parallel composition operator over
session types denoting the simultaneous access to a channel by two
or more processes. The proposed approach allows us to define a
semantically grounded theory of session types that does not
require the linear usage of channels. However, type preservation
and progress can only be guaranteed for processes that never
receive channels they already own. A number of examples show that
the resulting framework validates existing session type theories
and unifies them to some extent. },
title = {{On Projecting Processes into Session Types}},
publisher = {Cambridge University Press},
doi = {10.1017/S0960129511000405},
journal = {Mathematical Structures in Computer Science},
year = {2012},
pages = {237-289},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
