{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:39:21Z","timestamp":1742967561334,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_12","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"155-172","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Denotational and Operational Preciseness of Subtyping: A Roadmap"],"prefix":"10.1007","author":[{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"first","affiliation":[]},{"given":"Silvia","family":"Ghilezan","sequence":"additional","affiliation":[]},{"given":"Svetlana","family":"Jak\u0161i\u0107","sequence":"additional","affiliation":[]},{"given":"Jovanka","family":"Pantovi\u0107","sequence":"additional","affiliation":[]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"12_CR1","series-title":"Monographs in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, New York (1996)"},{"key":"12_CR2","unstructured":"van Bakel, S., Dezani-Ciancaglini, M., de\u2019 Liguoro, U., Motohama, Y.: The minimal relevant logic and the call-by-value lambda calculus. Technical Report TR-ARP-05-2000, The Australian National University (2000)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Barbanera, F., de Liguoro, U.: Two notions of sub-behaviour for session-based client\/server systems. In: Kutsia, T., Schreiner, W., Fern\u00e1ndez, M. (eds.) PPDP, pp. 155\u2013164. ACM (2010)","DOI":"10.1145\/1836089.1836109"},{"issue":"4","key":"12_CR4","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48(4), 931\u2013940 (1983)","journal-title":"J. Symbolic Logic"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-662-45917-1_4","volume-title":"Trustworthy Global Computing","author":"G Bernardi","year":"2014","unstructured":"Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 51\u201366. Springer, Heidelberg (2014)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/978-3-662-43951-7_6","volume-title":"Automata, Languages, and Programming","author":"MM Bonsangue","year":"2014","unstructured":"Bonsangue, M.M., Rot, J., Ancona, D., de Boer, F.S., Rutten, J.J.M.M.: A coalgebraic foundation for coinductive union types. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 62\u201373. Springer, Heidelberg (2014)"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-37036-6_19","volume-title":"Programming Languages and Systems","author":"L Caires","year":"2013","unstructured":"Caires, L., P\u00e9rez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 330\u2013349. Springer, Heidelberg (2013)"},{"issue":"1\u20133","key":"12_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/j.tcs.2008.01.049","volume":"398","author":"G Castagna","year":"2008","unstructured":"Castagna, G., De Nicola, R., Varacca, D.: Semantic subtyping for the pi-calculus. Theoret. Comput. Sci. 398(1\u20133), 217\u2013242 (2008)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: PPDP, pp. 219\u2013230. ACM (2009)","DOI":"10.1145\/1599410.1599437"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/11523468_3","volume-title":"Automata, Languages and Programming","author":"G Castagna","year":"2005","unstructured":"Castagna, G., Frisch, A.: A gentle introduction to semantic subtyping. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 30\u201334. Springer, Heidelberg (2005)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Chen, T.-C., Dezani-Ciancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: Chitil, O., King, A., Danvy, O. (eds.) PPDP, pp. 135\u2013146. ACM Press (2014)","DOI":"10.1145\/2643135.2643138"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-319-18941-3_4","volume-title":"Formal Methods for Multicore Programming","author":"M Coppo","year":"2015","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146\u2013178. Springer, Switzerland (2015)"},{"key":"12_CR13","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)"},{"issue":"5","key":"12_CR14","doi-asserted-by":"publisher","first-page":"1376","DOI":"10.1137\/S0097539794275860","volume":"27","author":"M Dezani-Ciancaglini","year":"1998","unstructured":"Dezani-Ciancaglini, M., de \u2019Liguoro, U., Piperno, A.: A filter model for concurrent lambda-calculus. SIAM J. Comput. 27(5), 1376\u20131419 (1998)","journal-title":"SIAM J. Comput."},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/978-3-319-08918-8_14","volume-title":"Rewriting and Typed Lambda Calculi","author":"M Dezani-Ciancaglini","year":"2014","unstructured":"Dezani-Ciancaglini, M., Ghilezan, S.: Preciseness of subtyping on intersection and union types. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 194\u2013207. Springer, Heidelberg (2014)"},{"key":"12_CR16","doi-asserted-by":"crossref","first-page":"29","DOI":"10.4204\/EPTCS.203.3","volume":"203","author":"Mariangiola Dezani-Ciancaglini","year":"2016","unstructured":"Dezani-Ciancaglini, M., Ghilezan, S., Jaksic, S., Pantovic, J., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. In: PLACES, EPTCS 203, pp. 29\u201344 (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"4","key":"12_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1391289.1391293","volume":"55","author":"A Frisch","year":"2008","unstructured":"Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55(4), 1\u201364 (2008)","journal-title":"J. ACM"},{"issue":"5","key":"12_CR18","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)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"3","key":"12_CR19","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1017\/S0960129514000231","volume":"26","author":"M Goto","year":"2016","unstructured":"Goto, M., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An extensible approach to session polymorphism. Math. Struct. Comput. Sci. 26(3), 465\u2013509 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"12_CR20","volume-title":"Practical Foundations for Programming Languages","author":"R Harper","year":"2013","unstructured":"Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press, Cambridge (2013)"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","volume":"22","author":"JR Hindley","year":"1983","unstructured":"Hindley, J.R.: The completeness theorem for typing lambda-terms. Theoret. Comput. Sci. 22, 1\u201317 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR22","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":"12_CR23","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In POPL, pp. 273\u2013284. ACM (2008). A full version will appear in Journal of the Association for Computing Machinery","DOI":"10.1145\/1328897.1328472"},{"issue":"1\u20133","key":"12_CR24","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(03)00325-6","volume":"311","author":"A Igarashi","year":"2004","unstructured":"Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoret. Comput. Sci. 311(1\u20133), 121\u2013163 (2004)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"12_CR25","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0304-3975(00)00351-0","volume":"272","author":"H Ishihara","year":"2002","unstructured":"Ishihara, H., Kurata, T.: Completeness of intersection and union type assignment systems for call-by-value lambda-models. Theoret. Comput. Sci. 272(1\u20132), 197\u2013221 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-40184-8_28","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"D Kouzapas","year":"2013","unstructured":"Kouzapas, D., Yoshida, N.: Globally governed session semantics. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 395\u2013409. Springer, Heidelberg (2013)"},{"key":"12_CR27","unstructured":"Ligatti, J., Blackburn, J., Nachtigal, M.: On subtyping-relation completeness, with an application to iso-recursive types. Technical report, University of South Florida (2014)"},{"issue":"2\/3","key":"12_CR28","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","volume":"76","author":"JC Mitchell","year":"1988","unstructured":"Mitchell, J.C.: Polymorphic type inference and containment. Inf. Comput. 76(2\/3), 211\u2013249 (1988)","journal-title":"Inf. Comput."},{"key":"12_CR29","unstructured":"Mostrous, D.: Session Types in Concurrent Calculi: Higher-Order Processes and Objects. PhD thesis, Imperial College London (2009)"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-02273-9_16","volume-title":"Typed Lambda Calculi and Applications","author":"D Mostrous","year":"2009","unstructured":"Mostrous, D., Yoshida, N.: Session-based communication optimisation for higher-order mobile processes. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 203\u2013218. Springer, Heidelberg (2009)"},{"key":"12_CR31","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 $$\\pi $$-calculus. Inf. Comput. 241, 227\u2013263 (2015)","journal-title":"Inf. Comput."},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-00590-9_23","volume-title":"Programming Languages and Systems","author":"D Mostrous","year":"2009","unstructured":"Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316\u2013332. Springer, Heidelberg (2009)"},{"key":"12_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-21464-6_9","volume-title":"Coordination Models and Languages","author":"L Padovani","year":"2011","unstructured":"Padovani, L.: Fair subtyping for multi-party session types. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 127\u2013141. Springer, Heidelberg (2011)"},{"key":"12_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/978-3-642-39212-2_34","volume-title":"Automata, Languages, and Programming","author":"L Padovani","year":"2013","unstructured":"Padovani, L.: Fair subtyping for open session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 373\u2013384. Springer, Heidelberg (2013)"},{"key":"12_CR35","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"issue":"1","key":"12_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.2001.2950","volume":"179","author":"J Tiuryn","year":"2002","unstructured":"Tiuryn, J., Urzyczyn, P.: The subtyping problem for second-order types is undecidable. Inf. Comput. 179(1), 1\u201318 (2002)","journal-title":"Inf. Comput."},{"issue":"3","key":"12_CR37","doi-asserted-by":"publisher","first-page":"1195","DOI":"10.2307\/2586625","volume":"64","author":"P Urzyczyn","year":"1999","unstructured":"Urzyczyn, P.: The emptiness problem for intersection types. J. Symbolic Logic 64(3), 1195\u20131215 (1999)","journal-title":"J. Symbolic Logic"},{"key":"12_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-540-30124-0_32","volume-title":"Computer Science Logic","author":"J Vouillon","year":"2004","unstructured":"Vouillon, J.: Subtyping union types. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 415\u2013429. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T12:23:00Z","timestamp":1720786980000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_12"}},"subtitle":["Dedicated to Frank de Boer on the Occasion of His 60th Birthday"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}