{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:01:07Z","timestamp":1762459267000},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T00:00:00Z","timestamp":1415923200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,9]]},"abstract":"<jats:p>We propose a refinement and a simplification of the behavioural semantics 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 \u2018session behaviours\u2019. 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 relations characterizes the \u2018usual\u2019 sub-behaviour relation from the literature. We then device an algorithmic 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 behaviours and sub-behaviour relations provide sound and complete semantics for CSP-subtyping, and for Gay and Hole subtyping as a by-product.<\/jats:p>","DOI":"10.1017\/s096012951400005x","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T23:05:39Z","timestamp":1416006339000},"page":"1339-1381","source":"Crossref","is-referenced-by-count":19,"title":["Sub-behaviour relations for session-based client\/server systems"],"prefix":"10.1017","volume":"25","author":[{"given":"FRANCO","family":"BARBANERA","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"UGO","family":"DE'LIGUORO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,11,14]]},"reference":[{"key":"S096012951400005X_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"S096012951400005X_ref4","doi-asserted-by":"crossref","unstructured":"Bernardi G. and Hennessy M. (2013a) Modelling session types using contracts. Mathematical Structures in Computer Science, To appear.","DOI":"10.1145\/2245276.2232097"},{"key":"S096012951400005X_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17660-8_53"},{"key":"S096012951400005X_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_6"},{"key":"S096012951400005X_ref26","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.12.5"},{"key":"S096012951400005X_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75698-9_14"},{"key":"S096012951400005X_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_3"},{"key":"S096012951400005X_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.05.002"},{"key":"S096012951400005X_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/1538917.1538920"},{"key":"S096012951400005X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_15"},{"key":"S096012951400005X_ref9","first-page":"451","article-title":"A foundational theory of contracts for multi-party service composition","volume":"89","author":"Bravetti","year":"2008","journal-title":"Fundamamenta Informaticae"},{"key":"S096012951400005X_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_15"},{"key":"S096012951400005X_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"},{"key":"S096012951400005X_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050168"},{"key":"S096012951400005X_ref29","doi-asserted-by":"crossref","unstructured":"Padovani L. (2013) Fair subtyping for multi-party session types. Mathematical Structures in Computer Science, To appear.","DOI":"10.1007\/978-3-642-39212-2_34"},{"key":"S096012951400005X_ref27","unstructured":"Padovani L. (2011) Private communication."},{"key":"S096012951400005X_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004318"},{"key":"S096012951400005X_ref6","unstructured":"Bernardi G. and Hennessy M. (2013c) Using higher-order contracts to model session types. In: http:\/\/adsabs.harvard.edu\/abs\/2013arXiv1310.6176B."},{"key":"S096012951400005X_ref21","first-page":"22","article-title":"Language primitives and type disciplines for structured communication-based programming","volume":"1381","author":"Honda","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"S096012951400005X_ref30","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1017\/S096012950007002X","article-title":"Typing and subtyping for mobile processes","volume":"6","author":"Pierce","year":"1996","journal-title":"Mathematical Structures in Computer Science"},{"key":"S096012951400005X_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/11841197_10"},{"key":"S096012951400005X_ref7","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","article-title":"Coinductive axiomatization of recursive type equality and subtyping","volume":"33","author":"Brandt","year":"1998","journal-title":"Fundamenta Informaticae"},{"key":"S096012951400005X_ref33","volume-title":"The \u03c0-Calculus: A Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S096012951400005X_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S096012951400005X_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_42"},{"key":"S096012951400005X_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0036936"},{"key":"S096012951400005X_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_5"},{"key":"S096012951400005X_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000405"},{"key":"S096012951400005X_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.12.005"},{"key":"S096012951400005X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_6"},{"key":"S096012951400005X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78663-4_18"},{"key":"S096012951400005X_ref3","doi-asserted-by":"crossref","unstructured":"Barbanera F. and de'Liguoro U. (2010) Two notions of sub-behaviour for session-based client\/server systems. In: Proceedings of PPDP'10. ACM SIGPLAN 155\u2013164.","DOI":"10.1145\/1836089.1836109"},{"key":"S096012951400005X_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.06.002"},{"key":"S096012951400005X_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951400005X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,26]],"date-time":"2020-08-26T21:47:36Z","timestamp":1598478456000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951400005X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,14]]},"references-count":34,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,9]]}},"alternative-id":["S096012951400005X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951400005x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,14]]}}}