{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T02:40:21Z","timestamp":1774579221768,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319309354","type":"print"},{"value":"9783319309361","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30936-1_5","type":"book-chapter","created":{"date-parts":[[2016,3,29]],"date-time":"2016-03-29T16:27:44Z","timestamp":1459268864000},"page":"95-108","source":"Crossref","is-referenced-by-count":12,"title":["Subtyping Supports Safe Session Substitution"],"prefix":"10.1007","author":[{"given":"Simon J.","family":"Gay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,25]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-71316-6_2","volume-title":"Programming Languages and Systems","author":"M Carbone","year":"2007","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2\u201317. Springer, Heidelberg (2007). \n                    http:\/\/dx.doi.org\/10.1007\/978-3-540-71316-6\/_2"},{"key":"5_CR2","unstructured":"Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 219\u2013230. ACM (2009). \n                    http:\/\/doi.acm.org\/10.1145\/1599410.1599437"},{"key":"5_CR3","unstructured":"Chen, T., Dezani-Ciancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: Proceedings of the 16th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 135\u2013146. ACM (2014). \n                    http:\/\/doi.acm.org\/10.1145\/2643135.2643138"},{"key":"5_CR4","unstructured":"Dardha, O.: Type Systems for Distributed Programs: Components and Sessions. Ph.D. thesis, University of Bologna (2014). \n                    https:\/\/tel.archives-ouvertes.fr\/tel-01020998"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: Proceedings of the 14th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 139\u2013150. ACM (2012)","DOI":"10.1145\/2370776.2370794"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-23217-6_19","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"R Demangeon","year":"2011","unstructured":"Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280\u2013296. Springer, Heidelberg (2011). \n                    http:\/\/dx.doi.org\/10.1007\/978-3-642-23217-6_19"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS), pp. 137\u2013146. IEEE (2002). \n                    http:\/\/dx.doi.org\/10.1109\/LICS.2002.1029823","DOI":"10.1109\/LICS.2002.1029823"},{"issue":"5","key":"5_CR8","doi-asserted-by":"publisher","first-page":"895","DOI":"10.1017\/S0960129508006944","volume":"18","author":"SJ Gay","year":"2008","unstructured":"Gay, S.J.: Bounded polymorphism in session types. Math. Struct. Comput. Sci. 18(5), 895\u2013930 (2008). \n                    http:\/\/dx.doi.org\/10.1017\/S0960129508006944","journal-title":"Math. Struct. Comput. Sci."},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49099-X_6","volume-title":"Programming Languages and Systems","author":"SJ Gay","year":"1999","unstructured":"Gay, S.J., Hole, M.: Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74\u201390. Springer, Heidelberg (1999)"},{"issue":"2\/3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"SJ Gay","year":"2005","unstructured":"Gay, S.J., Hole, M.J.: Subtyping for session types in the pi calculus. Acta Informatica 42(2\/3), 191\u2013225 (2005)","journal-title":"Acta Informatica"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 273\u2013284. ACM (2008)","DOI":"10.1145\/1328438.1328472"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR 1993","author":"K Honda","year":"1993","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509\u2013523. Springer, Heidelberg (1993)"},{"key":"5_CR13","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. 1381, pp. 122\u2013138. Springer, Heidelberg (1998)"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1007\/978-3-540-40007-3_26","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"Naoki Kobayashi","year":"2003","unstructured":"Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K. (ed.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 439\u2013453. Springer, Heidelberg (2003). \n                    http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/papers\/tutorial-type-extended.pdf"},{"issue":"5","key":"5_CR15","doi-asserted-by":"publisher","first-page":"914","DOI":"10.1145\/330249.330251","volume":"21","author":"N Kobayashi","year":"1999","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914\u2013947 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"5_CR16","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-73228-0_23","volume-title":"Typed Lambda Calculi and Applications","author":"D Mostrous","year":"2007","unstructured":"Mostrous, D., Yoshida, N.: Two session typing systems for higher-order mobile processes. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 321\u2013335. Springer, Heidelberg (2007). \n                    http:\/\/dx.doi.org\/10.1007\/978-3-540-73228-0_23"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.ic.2015.02.002","volume":"241","author":"D Mostrous","year":"2015","unstructured":"Mostrous, D., Yoshida, N.: Session typing and asynchronous subtyping for the higher-order \n                    \n                      \n                    \n                    $$\\pi $$\n                    \n                      \n                        \u03c0\n                      \n                    \n                  -calculus. Inf. Comput. 241, 227\u2013263 (2015). \n                    http:\/\/dx.doi.org\/10.1016\/j.ic.2015.02.002","journal-title":"Inf. Comput."},{"issue":"5","key":"5_CR19","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1017\/S096012950007002X","volume":"6","author":"BC Pierce","year":"1996","unstructured":"Pierce, B.C., Sangiorgi, D.: Typing and subtyping for mobile processes. Math. Struct. Comput. Sci. 6(5), 409\u2013454 (1996)","journal-title":"Math. Struct. Comput. Sci."},{"key":"5_CR20","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"5_CR21","volume-title":"The $$\\pi $$ \u03c0 -Calc","author":"D Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The \n                    \n                      \n                    \n                    $$\\pi $$\n                    \n                      \n                        \u03c0\n                      \n                    \n                  -Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/3-540-58184-7_118","volume-title":"PARLE \u201994 Parallel Architectures and Languages Europe","author":"K Takeuchi","year":"1994","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398\u2013413. Springer, Heidelberg (1994)"}],"container-title":["Lecture Notes in Computer Science","A List of Successes That Can Change the World"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30936-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T18:27:42Z","timestamp":1559413662000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30936-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319309354","9783319309361"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30936-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}