{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:54Z","timestamp":1781172354212,"version":"3.54.1"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T00:00:00Z","timestamp":1415577600000},"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":[[2016,2]]},"abstract":"<jats:p>We present a type system based on session types that works on a conventional pi calculus. Types are equipped with a constructor that describes the two ends of a single communication channel, this being the only type available for describing the behaviour of channels. Session types, in turn, describe the behaviour of each individual channel end, as usual. A novel notion of typing context split allows for typing processes not typable with extant type systems. We show that our system guarantees that typed processes do not engage in races for linear resources. We assess the expressiveness of the type system by providing three distinct encodings \u2013 from the pi calculus with polarized variables, from the pi calculus with accept and request primitives, and from the linear pi calculus \u2013 into our system. For each language we present operational and typing correspondences, showing that our system effectively subsumes foregoing works on linear and session types. In the case of the linear pi calculus we also provide a completeness result.<\/jats:p>","DOI":"10.1017\/s0960129514000176","type":"journal-article","created":{"date-parts":[[2014,11,10]],"date-time":"2014-11-10T07:01:26Z","timestamp":1415602886000},"page":"206-237","source":"Crossref","is-referenced-by-count":8,"title":["Linearity, session types and the Pi calculus"],"prefix":"10.1017","volume":"26","author":[{"given":"MARCO","family":"GIUNTI","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"VASCO THUDICHUM","family":"VASCONCELOS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,11,10]]},"reference":[{"key":"S0960129514000176_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_30"},{"key":"S0960129514000176_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"S0960129514000176_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"S0960129514000176_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S0960129514000176_ref15","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.61.7"},{"key":"S0960129514000176_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0960129514000176_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000405"},{"key":"S0960129514000176_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"S0960129514000176_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_5"},{"key":"S0960129514000176_ref19","first-page":"22","article-title":"Language primitives and type disciplines for structured communication-based programming","volume":"1381","author":"Honda","year":"1998","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"S0960129514000176_ref2","first-page":"100","volume-title":"AMAST","author":"Bruni","year":"2008"},{"key":"S0960129514000176_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.016"},{"key":"S0960129514000176_ref27","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0960129514000176_ref33","first-page":"73","article-title":"Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication","volume":"171","author":"Yoshida","year":"2007","journal-title":"ENTCS"},{"key":"S0960129514000176_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14458-5_1"},{"key":"S0960129514000176_ref30","first-page":"53","article-title":"Sessions, from types to programming languages","volume":"103","author":"Vasconcelos","year":"2011","journal-title":"Bulletin of the EATCS"},{"key":"S0960129514000176_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"S0960129514000176_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"S0960129514000176_ref1","first-page":"82","article-title":"A type system for flexible role assignment in multiparty communicating systems","volume":"8191","author":"Baltazar","year":"2013","journal-title":"Springer LNCS"},{"key":"S0960129514000176_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/11580850_16"},{"key":"S0960129514000176_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.010"},{"key":"S0960129514000176_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72952-5_1"},{"key":"S0960129514000176_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"S0960129514000176_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_10"},{"key":"S0960129514000176_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"S0960129514000176_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1218063.1217953"},{"key":"S0960129514000176_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S0960129514000176_ref16","unstructured":"Giunti M. , Honda K. , Vasconcelos V. T. and Yoshida N. (2009) Session-based type discipline for pi calculus with matching. In: PLACES."},{"key":"S0960129514000176_ref24","article-title":"The polyadic \u03c0-calculus: A tutorial","volume":"94","author":"Milner","year":"1993","journal-title":"Springer Series F. NATO ASI"},{"key":"S0960129514000176_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"S0960129514000176_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"S0960129514000176_ref13","first-page":"299","volume-title":"POPL","author":"Gay","year":"2010"},{"key":"S0960129514000176_ref28","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"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000176","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T01:40:19Z","timestamp":1566006019000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000176\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,10]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,2]]}},"alternative-id":["S0960129514000176"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000176","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,10]]}}}