{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T17:32:56Z","timestamp":1781976776109,"version":"3.54.5"},"reference-count":55,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T00:00:00Z","timestamp":1424649600000},"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,3]]},"abstract":"<jats:p>Session types describe and constrain the input\/output behaviour of systems. Existing session typing systems have limited support for polymorphism. For example, existing systems cannot provide the most general type for a generic proxy process that forwards messages between two channels. We provide a polymorphic session typing system for the \u03c0 calculus, and demonstrate the utility of session-type-level functions in combination with polymorphic session typing. The type system guarantees subject reduction and safety properties, but not deadlock freedom. We describe a formalization of the type system in Coq. The proofs of subject reduction and safety properties, as well as typing of example processes, have been mechanically verified.<\/jats:p>","DOI":"10.1017\/s0960129514000231","type":"journal-article","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T05:47:02Z","timestamp":1424670422000},"page":"465-509","source":"Crossref","is-referenced-by-count":14,"title":["An extensible approach to session polymorphism"],"prefix":"10.1017","volume":"26","author":[{"given":"MATTHEW","family":"GOTO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"RADHA","family":"JAGADEESAN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALAN","family":"JEFFREY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"CORIN","family":"PITCHER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JAMES","family":"RIELY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2015,2,23]]},"reference":[{"key":"S0960129514000231_ref14","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou P.-M. and Yoshida N. (2011) Dynamic multirole session types. In: Symposium on Principles of programming languages 435\u2013446.","DOI":"10.1145\/1926385.1926435"},{"key":"S0960129514000231_ref28","unstructured":"Giunti M. , Honda K. , Vasconcelos V. T. and Yoshida N. (2009) Session-based type discipline for pi calculus with matching. Available at http:\/\/homepages.di.fc.ul.pt\/~vv\/papers\/giunti.honda.etal_session-based-pi-matching.pdf."},{"key":"S0960129514000231_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006944"},{"key":"S0960129514000231_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"S0960129514000231_ref17","doi-asserted-by":"crossref","unstructured":"Dezani-Ciancaglini M. , de Liguoro U. and Yoshida N. (2007a) On progress for structured communications. In: TGC. Springer Lecture Notes in Computer Science 257\u2013275.","DOI":"10.1007\/978-3-540-78663-4_18"},{"key":"S0960129514000231_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"S0960129514000231_ref54","first-page":"273","volume-title":"International Conference on Functional Programming","author":"Wadler","year":"2012"},{"key":"S0960129514000231_ref45","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004653"},{"key":"S0960129514000231_ref36","doi-asserted-by":"crossref","unstructured":"Kiselyov O. , Peyton Jones S. and Shan C.-C. (2010) Fun with type functions (version 3). Presented at Tony Hoare's 75th birthday celebration.","DOI":"10.1007\/978-1-84882-912-1_14"},{"key":"S0960129514000231_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_17"},{"key":"S0960129514000231_ref29","first-page":"73","volume-title":"Logics and Languages for Reliability and Security, NATO Science for Peace and Security Series - D: Information and Communication Security volume 25","author":"Gordon","year":"2010"},{"key":"S0960129514000231_ref27","doi-asserted-by":"crossref","unstructured":"Gay S. J. , Vasconcelos V. T. , Ravara A. , Gesbert N. and Caldeira A. Z. (2010) Modular session types for distributed object-oriented programming. In: Symposium on Principles of programming languages 299\u2013312.","DOI":"10.1145\/1706299.1706335"},{"key":"S0960129514000231_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72952-5_1"},{"key":"S0960129514000231_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"S0960129514000231_ref2","doi-asserted-by":"crossref","unstructured":"Aydemir B. , Chargu\u00e9raud A. , Pierce B. C. , Pollack R. and Weirich S. (2008) Engineering formal metatheory. In: Symposium on Principles of programming languages 3\u201315.","DOI":"10.1145\/1328438.1328443"},{"key":"S0960129514000231_ref53","unstructured":"Vasconcelos V. T. , Giunti M. , Yoshida N. and Honda K. (2010) Type safety without subject reduction for session types. Available at http:\/\/www.di.fc.ul.pt\/~vv\/papers\/vasconcelos.giunti.etal_type-safety-session-types.pdf."},{"key":"S0960129514000231_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"S0960129514000231_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.012"},{"key":"S0960129514000231_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680400543X"},{"key":"S0960129514000231_ref46","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe","year":"1997"},{"key":"S0960129514000231_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0960129514000231_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S0960129514000231_ref44","doi-asserted-by":"crossref","unstructured":"Pucella R. and Tov J. A. (2008) Haskell session types with (almost) no class. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, 25\u201336.","DOI":"10.1145\/1411286.1411290"},{"key":"S0960129514000231_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"S0960129514000231_ref32","doi-asserted-by":"crossref","unstructured":"Honda K. , Yoshida N. and Carbone M. (2008) Multiparty asynchronous session types. In: Symposium on Principles of programming languages 273\u2013284.","DOI":"10.1145\/1328438.1328472"},{"key":"S0960129514000231_ref40","volume-title":"Logic and Algebra of Specification","author":"Milner","year":"1991"},{"key":"S0960129514000231_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"S0960129514000231_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"S0960129514000231_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0960129514000231_ref9","first-page":"219","volume-title":"Symposium on Principles and Practice of Declarative Programming","author":"Castagna","year":"2009"},{"key":"S0960129514000231_ref22","first-page":"268","volume-title":"Proceedings of the SIGPLAN '91 Symposium on Language Design and Implementation","author":"Freeman","year":"1991"},{"key":"S0960129514000231_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24836-1_5"},{"key":"S0960129514000231_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1010832.1010837"},{"key":"S0960129514000231_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/276393.278524"},{"key":"S0960129514000231_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/362946.362970"},{"key":"S0960129514000231_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.08.004"},{"key":"S0960129514000231_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"S0960129514000231_ref23","doi-asserted-by":"crossref","unstructured":"Gay S. J. (2001) A framework for the formalisation of \u03c0 calculus type systems in Isabelle\/HOL. In: Proceedings of 14th Theorem Proving in Higher Order Logics 217\u2013232.","DOI":"10.1007\/3-540-44755-5_16"},{"key":"S0960129514000231_ref12","unstructured":"Coquand T. (1992) Pattern matching with dependent types. In: Nordstr\u00f6m B. , Petersson K. and Plotkin G. (eds.) Electronic Proceedings of the 3rd Annual BRA Workshop on Logical Frameworks 66\u201379. Available from http:\/\/www.lfcs.inf.ed.ac.uk\/research\/types-bra\/proc\/."},{"key":"S0960129514000231_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.010"},{"key":"S0960129514000231_ref49","first-page":"117","volume-title":"International Conference on Functional Programming","author":"Tobin-Hochstadt","year":"2010"},{"key":"S0960129514000231_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44929-9_30"},{"key":"S0960129514000231_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"S0960129514000231_ref35","unstructured":"Jeffrey A. S. A. and Rathke J. (2011) The lax braided structure of streaming I\/O. In: Proceedings Conference of Computer Science Logic 292\u2013306."},{"key":"S0960129514000231_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14458-5_1"},{"key":"S0960129514000231_ref55","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"},{"key":"S0960129514000231_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_10"},{"key":"S0960129514000231_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"S0960129514000231_ref47","unstructured":"Sackman M. and Eisenbach S. (2008) Session types in Haskell: Updating message passing for the 21st century. Available at http:\/\/hdl.handle.net\/10044\/1\/5918."},{"key":"S0960129514000231_ref30","unstructured":"Goto M. , Jagadeesan R. , Jeffrey A. , Pitcher C. and Riely J. (2011) Coq formalization of extensible polymorphic session types. Available at http:\/\/fpl.cs.depaul.edu\/projects\/xpol\/."},{"key":"S0960129514000231_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S0960129514000231_ref50","first-page":"161","volume-title":"Symposium on Principles and Practices of Declarative Programming","author":"Toninho","year":"2011"},{"key":"S0960129514000231_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01918-0_4"},{"key":"S0960129514000231_ref6","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.59.5"},{"key":"S0960129514000231_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000231","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T04:31:17Z","timestamp":1566361877000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000231\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,23]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["S0960129514000231"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000231","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,23]]}}}