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).

Sub-behaviour relations for session-based client/server systems

BARBANERA, Franco;DE' LIGUORO, Ugo
2014-01-01

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).
2014
25
6
1339
1381
http://journals.cambridge.org/action/displayJournal?jid=MSC
Barbanera, Franco; De'Liguoro, Ugo
File in questo prodotto:
File Dimensione Formato  
CSP-draft.pdf

Accesso aperto

Descrizione: Articolo principale
Tipo di file: PREPRINT (PRIMA BOZZA)
Dimensione 387.38 kB
Formato Adobe PDF
387.38 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1526465
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 25
  • ???jsp.display-item.citation.isi??? 22
social impact