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

摘要

We propose a refinement and a simplification of the behavioural semantics of session types,rnbased on the concepts of compliance and sub-behaviour from the theory of web contracts.rnWe introduce three relations on a suitable class of behaviours with higher-order input/rnoutput, called ‘session behaviours’. Such relations, depending on each other, represent thernidea of sub-behaviour from the point of view of a client, a server or a peer, respectively. Arnrestriction of the intersection of the first two relations characterizes the ‘usual’ sub-behaviourrnrelation from the literature. We then device an algorithmic formal system for three subtypingrnrelations (dubbed CSP-subtyping) for session types that takes into account the role playedrnby a user of a channel during an interaction, so extending Gay and Hole subtyping theory.rnWe show that our session behaviours and sub-behaviour relations provide sound andrncomplete semantics for CSP-subtyping, and for Gay and Hole subtyping as a by-product.