Barbanera-deLiguoro-MSCS (Article)
|
Author(s) | Franco Barbanera and Ugo de' Liguoro |
Title | « Sub-behaviour relations for session-based client/server systems » |
Journal | MSCS |
Volume | 25 |
Number | 6 |
Page(s) | 1339--1381 |
Year | 2015 |
Note | to appear |
Abstract |
We propose a refinement and a simplification of the behavioural se- mantics of session types, based on the concepts of compliance and sub- behaviour from the theory of web contracts. We introduce three relations on a suitable class of behaviours with higher-order input/output, called session behaviors. Such relations, depending on each other, represent the idea of sub-behaviour from the point of view of a client, a server or a peer, respectively. A restriction of the intersection of the first two characterizes the usual sub-behaviour relation (from the literature). We then device a formal system for three subtyping relations (dubbed CSP- subtyping) for session types that takes into account the role played by a user of a channel during an interaction, so extending Gay and Hole subtyping theory. We show that our session behaviors and sub-behaviour relations provide a sound and complete semantics for CSP-subtyping (and for Gay and Hole subtyping as a by-product). |
Download the complete article:
@article{Barbanera-deLiguoro-MSCS,
number = {6},
volume = {25},
author = {Franco Barbanera and Ugo de' Liguoro},
note = {to appear},
tag = {{Mathematical Structures in Computer Science}},
localfile = {http://www.di.unito.it/~deligu/papers/CSP-draft.pdf},
title = {{Sub-behaviour relations for session-based client/server systems}},
abstract = {We propose a refinement and a simplification of the behavioural
se- mantics of session types, based on the concepts of compliance
and sub- behaviour from the theory of web contracts. We introduce
three relations on a suitable class of behaviours with
higher-order input/output, called {\em session behaviors}. Such
relations, depending on each other, represent the idea of
sub-behaviour from the point of view of a client, a server or a
peer, respectively. A restriction of the intersection of the first
two characterizes the usual sub-behaviour relation (from the
literature). We then device a formal system for three subtyping
relations (dubbed CSP- subtyping) for session types that takes
into account the role played by a user of a channel during an
interaction, so extending Gay and Hole subtyping theory. We show
that our session behaviors and sub-behaviour relations provide a
sound and complete semantics for CSP-subtyping (and for Gay and
Hole subtyping as a by-product).},
journal = {MSCS},
year = {2015},
pages = {1339--1381},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)