{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T03:22:09Z","timestamp":1771471329497,"version":"3.50.1"},"reference-count":35,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2008,10,1]],"date-time":"2008-10-01T00:00:00Z","timestamp":1222819200000},"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":[[2008,10]]},"abstract":"<jats:p>Session types allow high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. In collaboration with Malcolm Hole, we previously introduced a notion of subtyping for session types, which was formulated for an extended pi calculus. Subtyping allows one part of a system, for example, a server, to be refined without invalidating type-correctness of other parts, for example, clients. In this paper we introduce bounded polymorphism, which is based on the same notion of subtyping, in order to support more precise and flexible specifications of protocols; in particular, a choice of type in one message may affect the types of future messages. We formalise the syntax, operational semantics and typing rules of an extended pi calculus, and prove that typechecking guarantees the absence of run-time communication errors. We study algorithms for checking instances of the subtype relation in two versions of our system, which we call Kernel<jats:italic>S<\/jats:italic><jats:sub>\u2264<\/jats:sub>and Full<jats:italic>S<\/jats:italic><jats:sub>\u2264<\/jats:sub>, and establish that subtyping in Kernel<jats:italic>S<\/jats:italic><jats:sub>\u2264<\/jats:sub>is decidable, and that subtyping in Full<jats:italic>S<\/jats:italic><jats:sub>\u2264<\/jats:sub>is undecidable.<\/jats:p>","DOI":"10.1017\/s0960129508006944","type":"journal-article","created":{"date-parts":[[2008,10,6]],"date-time":"2008-10-06T10:02:51Z","timestamp":1223287371000},"page":"895-930","source":"Crossref","is-referenced-by-count":39,"title":["Bounded polymorphism in session types"],"prefix":"10.1017","volume":"18","author":[{"given":"SIMON J.","family":"GAY","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2008,10,1]]},"reference":[{"key":"S0960129508006944_ref31","first-page":"583","article-title":"Typing the behavior of software components using session types","volume":"73","author":"Vallecillo","year":"2006","journal-title":"Fundamenta Informaticae"},{"key":"S0960129508006944_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S0960129508006944_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0960129508006944_ref26","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"Pierce","year":"2000"},{"key":"S0960129508006944_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/337244.337261"},{"key":"S0960129508006944_ref23","volume-title":"Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science","author":"Pierce","year":"1993"},{"key":"S0960129508006944_ref22","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0960129508006944_ref15","unstructured":"Katiyar D. and Sankar S. (1992) Completely bounded quantification is decidable. In: Proceedings of the ACM SIGPLAN Workshop on ML and its Applications."},{"key":"S0960129508006944_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_32"},{"key":"S0960129508006944_ref35","unstructured":"Yoshida N. and Vasconcelos V. T. (2006) Language primitives and type discipline for structured communication-based programming revisited \u2013 two systems for higher-order session communication. In: Procedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT 2006). Electronic Notes in Theoretical Computer Science."},{"key":"S0960129508006944_ref6","volume-title":"EuroSys 2006","author":"F\u00e4hndrich","year":"2006"},{"key":"S0960129508006944_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0960129508006944_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60218-6_8"},{"key":"S0960129508006944_ref8","volume-title":"Proceedings of the 20th ACM Symposium on Principles of Programming Languages","author":"Gay","year":"1993"},{"key":"S0960129508006944_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"S0960129508006944_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_36"},{"key":"S0960129508006944_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129508006944_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24836-1_5"},{"key":"S0960129508006944_ref28","volume-title":"The \u03c0-calculus: a Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S0960129508006944_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0960129508006944_ref30","unstructured":"Turner D. N. (1996) The Polymorphic Pi-Calculus: Theory and Implementation, Ph.D. thesis, University of Edinburgh."},{"key":"S0960129508006944_ref21","unstructured":"Neubauer M. and Thiemann P. (2004b) Session types for asynchronous communication (manuscript)."},{"key":"S0960129508006944_ref24","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":"S0960129508006944_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"S0960129508006944_ref18","unstructured":"Milner R. (1991) The polyadic \u03c0-calculus: a tutorial. Technical Report 91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh."},{"key":"S0960129508006944_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680400543X"},{"key":"S0960129508006944_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_6"},{"key":"S0960129508006944_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"S0960129508006944_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"S0960129508006944_ref2","unstructured":"Carbone M. , Honda K. , Yoshida N. , Milner R. , Brown G. and Ross-Talbot S. (2006) A theoretical basis of communication-centred concurrent programming. W3C Web Services Choreography Working Group Report. www.w3.org\/2002\/ws\/chor\/edcopies\/theory\/note.pdf."},{"key":"S0960129508006944_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/11580850_16"},{"key":"S0960129508006944_ref7","first-page":"61","volume-title":"Proceedings of the ACM Symposium on Principles and Practice of Declarative Programming","author":"Garralda","year":"2006"},{"key":"S0960129508006944_ref11","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur, Ph.D. thesis, University of Paris VII."},{"key":"S0960129508006944_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"S0960129508006944_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508006944","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T08:36:38Z","timestamp":1557822998000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508006944\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["S0960129508006944"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508006944","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,10]]}}}