{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:53:17Z","timestamp":1770288797824,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_19","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"330-349","source":"Crossref","is-referenced-by-count":37,"title":["Behavioral Polymorphism and Parametricity in Session-Based Communication"],"prefix":"10.1007","author":[{"given":"Lu\u00eds","family":"Caires","sequence":"first","affiliation":[]},{"given":"Jorge A.","family":"P\u00e9rez","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[]},{"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-36576-1_7","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Berger","year":"2003","unstructured":"Berger, M., Honda, K., Yoshida, N.: Genericity and the \u03c0-Calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 103\u2013119. Springer, Heidelberg (2003)"},{"issue":"2-3","key":"19_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s00236-005-0175-1","volume":"42","author":"M. Berger","year":"2005","unstructured":"Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-calculus. Acta Inf.\u00a042(2-3), 83\u2013141 (2005)","journal-title":"Acta Inf."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Bono, V., Padovani, L.: Polymorphic endpoint types for copyless message passing. In: Proc. of ICE 2011. EPTCS, vol.\u00a059, pp. 52\u201367 (2011)","DOI":"10.4204\/EPTCS.59.5"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Bono, V., Padovani, L.: Typing copyless message passing. Logical Methods in Computer Science 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:17)2012"},{"key":"19_CR5","unstructured":"Caires, L., P\u00e9rez, J.A., Pfenning, F., Toninho, B.: Relational parametricity for polymorphic session types. Tech. rep., CMU-CS-12-108, Carnegie Mellon Univ. (April 2012)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L. Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 222\u2013236. Springer, Heidelberg (2010)"},{"key":"19_CR7","unstructured":"Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types (2012), under Revision - http:\/\/www.cs.cmu.edu\/~fp\/papers\/sessions12.pdf"},{"key":"19_CR8","first-page":"1","volume-title":"TLDI 2012","author":"L. Caires","year":"2012","unstructured":"Caires, L., Pfenning, F., Toninho, B.: Towards concurrent type theory. In: TLDI 2012, pp. 1\u201312. ACM, New York (2012)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session Types Revisited. In: PPDP, pp. 139\u2013150. ACM (2012)","DOI":"10.1145\/2370776.2370794"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-74792-5_10","volume-title":"Formal Methods for Components and Objects","author":"M. Dezani-Ciancaglini","year":"2007","unstructured":"Dezani-Ciancaglini, M., Giachino, E., Drossopoulou, S., Yoshida, N.: Bounded Session Types for Object Oriented Languages. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol.\u00a04709, pp. 207\u2013245. Springer, Heidelberg (2007)"},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"S. Gay","year":"2005","unstructured":"Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf.\u00a042, 191\u2013225 (2005)","journal-title":"Acta Inf."},{"issue":"5","key":"19_CR12","doi-asserted-by":"publisher","first-page":"895","DOI":"10.1017\/S0960129508006944","volume":"18","author":"S.J. Gay","year":"2008","unstructured":"Gay, S.J.: Bounded polymorphism in session types. Math. Struc. in Comp. Sci.\u00a018(5), 895\u2013930 (2008)","journal-title":"Math. Struc. in Comp. Sci."},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse, et son application \u00e0 l\u2019\u00e9limination de coupures dans l\u2019analyse et la th\u00e9orie des types. In: Proc. of the 2nd Scandinavian Logic Symposium, pp. 63\u201392. North-Holland Publishing Co. (1971)","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"19_CR14","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1989)"},{"key":"19_CR15","unstructured":"Goto, M., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An Extensible Approach to Session Polymorphism (2012), http:\/\/fpl.cs.depaul.edu\/projects\/xpol\/"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139342131"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR\u201993","author":"K. Honda","year":"1993","unstructured":"Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 509\u2013523. Springer, Heidelberg (1993)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K. Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, pp. 122\u2013138. Springer, Heidelberg (1998)"},{"issue":"2-3","key":"19_CR19","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/j.tcs.2007.09.020","volume":"390","author":"A. Jeffrey","year":"2008","unstructured":"Jeffrey, A., Rathke, J.: Full abstraction for polymorphic pi-calculus. Theor. Comput. Sci.\u00a0390(2-3), 171\u2013196 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-642-28869-2_27","volume-title":"Programming Languages and Systems","author":"J.A. P\u00e9rez","year":"2012","unstructured":"P\u00e9rez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear Logical Relations for Session-Based Concurrency. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 539\u2013558. Springer, Heidelberg (2012)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-25379-9_4","volume-title":"Certified Programs and Proofs","author":"F. Pfenning","year":"2011","unstructured":"Pfenning, F., Caires, L., Toninho, B.: Proof-Carrying Code in a Session-Typed Process Calculus. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 21\u201336. Springer, Heidelberg (2011)"},{"issue":"3","key":"19_CR22","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1145\/337244.337261","volume":"47","author":"B.C. Pierce","year":"2000","unstructured":"Pierce, B.C., Sangiorgi, D.: Behavioral equivalence in the polymorphic pi-calculus. J. ACM\u00a047(3), 531\u2013584 (2000)","journal-title":"J. ACM"},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Programming Symposium, Proceedings Colloque sur la Programmation","author":"J.C. Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Programming Symposium, Proceedings Colloque sur la Programmation, pp. 408\u2013423. Springer, London (1974)"},{"key":"19_CR24","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 1983, pp. 513\u2013523. Elsevier Science Publishers B. V. (1983)"},{"key":"19_CR25","volume-title":"The \u03c0-calculus: A Theory of Mobile Processes","author":"D. Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus: A Theory of Mobile Processes. Cambridge University Press, New York (2001)"},{"key":"19_CR26","first-page":"161","volume-title":"Proc. of PPDP 2011","author":"B. Toninho","year":"2011","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proc. of PPDP 2011, pp. 161\u2013172. ACM, New York (2011)"},{"key":"19_CR27","unstructured":"Turner, D.: The polymorphic pi-calculus: Theory and implementation. Tech. rep., ECS-LFCS-96-345, Univ. of Edinburgh (1996)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as sessions. In: Thiemann, P., Findler, R.B. (eds.) ICFP, pp. 273\u2013286. ACM (2012)","DOI":"10.1145\/2398856.2364568"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Washburn, G., Weirich, S.: Generalizing parametricity using information-flow. In: LICS, pp. 62\u201371. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.20"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-642-17164-2_24","volume-title":"Programming Languages and Systems","author":"J. Zhao","year":"2010","unstructured":"Zhao, J., Zhang, Q., Zdancewic, S.: Relational Parametricity for a Polymorphic Linear Lambda Calculus. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 344\u2013359. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:32:35Z","timestamp":1745962355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}