{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:12Z","timestamp":1781172312266,"version":"3.54.1"},"reference-count":35,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,12,8]],"date-time":"2009-12-08T00:00:00Z","timestamp":1260230400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2010,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Session types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static typechecking. Applications include network protocols, business processes and operating system services. In this paper we define a multithreaded functional language with session types, which unifies, simplifies and extends previous work. There are four main contributions. First is an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second, we prove that the session type of a channel gives an upper bound on the necessary size of the buffer. Third, session types are manipulated by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Fourth, a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting), and a novel form of subtyping between standard and linear function types, which allows the typechecker to handle linear types conveniently. Our new approach significantly simplifies session types in the functional setting, clarifies their essential features and provides a secure foundation for language developments such as polymorphism and object-orientation.<\/jats:p>","DOI":"10.1017\/s0956796809990268","type":"journal-article","created":{"date-parts":[[2009,12,8]],"date-time":"2009-12-08T10:46:04Z","timestamp":1260269164000},"page":"19-50","source":"Crossref","is-referenced-by-count":147,"title":["Linear type theory for asynchronous session types"],"prefix":"10.1017","volume":"20","author":[{"given":"SIMON J.","family":"GAY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"VASCO T.","family":"VASCONCELOS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2009,12,8]]},"reference":[{"key":"S0956796809990268_ref29","first-page":"583","article-title":"Typing the behavior of software components using session types","volume":"73","author":"Vallecillo","year":"2006","journal-title":"Fundam. Inform."},{"key":"S0956796809990268_ref17","first-page":"282","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Grossman","year":"2002"},{"key":"S0956796809990268_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"S0956796809990268_ref4","first-page":"1","volume-title":"Proceedings of the 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)","author":"Coppo","year":"2007"},{"key":"S0956796809990268_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680400543X"},{"key":"S0956796809990268_ref10","volume-title":"Subtyping Between Standard and Linear Function Types","author":"Gay","year":"2006"},{"key":"S0956796809990268_ref1","doi-asserted-by":"publisher","DOI":"10.1142\/p132"},{"key":"S0956796809990268_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"S0956796809990268_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_17"},{"key":"S0956796809990268_ref31","first-page":"497","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR)","author":"Vasconcelos","year":"2004"},{"key":"S0956796809990268_ref6","first-page":"328","volume-title":"Proceedings of the European Conference on Object-Oriented Languages (ECOOP)","author":"Dezani-Ciancaglini","year":"2006"},{"key":"S0956796809990268_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006944"},{"key":"S0956796809990268_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24836-1_5"},{"key":"S0956796809990268_ref5","first-page":"59","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"DeLine","year":"2001"},{"key":"S0956796809990268_ref33","first-page":"3","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker","year":"2005"},{"key":"S0956796809990268_ref24","unstructured":"Neubauer M. & Thiemann P. (2004c) Session Types for Asynchronous Communication. [online] Available at: http:\/\/www.informatik.uni-freiburg.de\/~thiemann\/papers\/stac.ps.gz Accessed 17 November 2009."},{"key":"S0956796809990268_ref16","first-page":"13","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)","author":"Grossman","year":"2003"},{"key":"S0956796809990268_ref8","first-page":"177","volume-title":"Proceedings of the EuroSys Conference, SIGOPS Operating Systems Review","author":"F\u00e4hndrich","year":"2006"},{"key":"S0956796809990268_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/11580850_16"},{"key":"S0956796809990268_ref15","volume-title":"Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Gay","year":"2010"},{"key":"S0956796809990268_ref25","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/1040305.1040324","volume-title":"Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Neubauer","year":"2005"},{"key":"S0956796809990268_ref35","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":"S0956796809990268_ref27","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0956796809990268_ref14","volume-title":"Session Types for Inter-Process Communication","author":"Gay","year":"2003"},{"key":"S0956796809990268_ref9","first-page":"13","volume-title":"Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"F\u00e4hndrich","year":"2002"},{"key":"S0956796809990268_ref34","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"S0956796809990268_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.016"},{"key":"S0956796809990268_ref13","volume-title":"Asynchronous Functional Session Types","author":"Gay","year":"2007"},{"key":"S0956796809990268_ref21","first-page":"305","volume-title":"Proceedings of the IEEE International Conference on Software Engineering and Formal Methods","author":"Lanese","year":"2007"},{"key":"S0956796809990268_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S0956796809990268_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"S0956796809990268_ref18","first-page":"509","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR)","author":"Honda","year":"1993"},{"key":"S0956796809990268_ref32","unstructured":"W3C. (2005) Services choreography description language version 1.0 [online]. Available at: http:\/\/www.w3.org\/TR\/2005\/CR-ws-cdl-10\/ Accessed 17 November 2009."},{"key":"S0956796809990268_ref20","first-page":"273","volume-title":"Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Honda","year":"2008"},{"key":"S0956796809990268_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796809990268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:21Z","timestamp":1779834981000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796809990268\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12,8]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,1]]}},"alternative-id":["S0956796809990268"],"URL":"https:\/\/doi.org\/10.1017\/s0956796809990268","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12,8]]}}}