{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:11:07Z","timestamp":1743070267291,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319924076"},{"type":"electronic","value":"9783319924083"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92408-3_2","type":"book-chapter","created":{"date-parts":[[2018,5,26]],"date-time":"2018-05-26T17:08:42Z","timestamp":1527354522000},"page":"21-50","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Foundations of Coordination and Contracts and Their Contribution to Session Type Theory"],"prefix":"10.1007","author":[{"given":"Mario","family":"Bravetti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianluigi","family":"Zavattaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,27]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Barbanera, F., de\u2019Liguoro, U.: Two notions of sub-behaviour for session-based client\/server systems. In: Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2010, pp. 155\u2013164. ACM (2010)","DOI":"10.1145\/1836089.1836109"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-20401-2_13","volume-title":"Rigorous Software Engineering for Service-Oriented Systems","author":"M Boreale","year":"2011","unstructured":"Boreale, M., Bravetti, M.: Advanced mechanisms for service composition, query and discovery. In: Wirsing, M., H\u00f6lzl, M. (eds.) Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582, pp. 282\u2013301. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20401-2_13"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1016\/j.ic.2017.07.010","volume":"256","author":"M Bravetti","year":"2017","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300\u2013320 (2017)","journal-title":"Inf. Comput."},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.tcs.2018.02.010","volume":"722","author":"M Bravetti","year":"2018","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci. 722, 19\u201351 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-75698-9_14","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"M Bravetti","year":"2007","unstructured":"Bravetti, M., Zavattaro, G.: Contract based multi-party service composition. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 207\u2013222. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75698-9_14"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-72794-1_6","volume-title":"Coordination Models and Languages","author":"M Bravetti","year":"2007","unstructured":"Bravetti, M., Zavattaro, G.: A theory for strong service compliance. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 96\u2013112. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72794-1_6"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-77351-1_4","volume-title":"Software Composition","author":"M Bravetti","year":"2007","unstructured":"Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34\u201350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77351-1_4"},{"issue":"4","key":"2_CR9","first-page":"451","volume":"89","author":"M Bravetti","year":"2008","unstructured":"Bravetti, M., Zavattaro, G.: A foundational theory of contracts for multi-party service composition. Fundamenta Informaticae 89(4), 451\u2013478 (2008)","journal-title":"Fundamenta Informaticae"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-642-01364-5_3","volume-title":"Web Services and Formal Methods","author":"M Bravetti","year":"2009","unstructured":"Bravetti, M., Zavattaro, G.: Contract compliance and choreography conformance in the presence of message queues. In: Bruni, R., Wolf, K. (eds.) WS-FM 2008. LNCS, vol. 5387, pp. 37\u201354. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01364-5_3"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"12","DOI":"10.4204\/EPTCS.168.2","volume":"168","author":"Mario Bravetti","year":"2014","unstructured":"Bravetti, M., Zavattaro, G.: Choreographies and behavioural contracts on the way to dynamic updates. In: Proceedings of the 1st Workshop on Logics and Model-checking for Self-* Systems, MOD* 2014. EPTCS, vol. 168, pp. 12\u201331 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-63383-9_84","volume-title":"Coordination Languages and Models","author":"A Brogi","year":"1997","unstructured":"Brogi, A., Jacquet, J.-M.: Modeling coordination via asynchronous communication. In: Garlan, D., Le M\u00e9tayer, D. (eds.) COORDINATION 1997. LNCS, vol. 1282, pp. 238\u2013255. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63383-9_84"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/S1571-0661(05)80467-0","volume":"7","author":"Nadia Busi","year":"1997","unstructured":"Busi, N., Gorrieri, R., Zavattaro, G.: On the Turing equivalence of Linda coordination primitives. In: Proceedings of 4th Workshop on Expressiveness in Concurrency, EXPRESS 1997. Elsevier (1997). Electr. Notes Theor. Comput. Sci. 7","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/3-540-63383-9_82","volume-title":"Coordination Languages and Models","author":"N Busi","year":"1997","unstructured":"Busi, N., Gorrieri, R., Zavattaro, G.: Three semantics of the output operation for generative communication. In: Garlan, D., Le M\u00e9tayer, D. (eds.) COORDINATION 1997. LNCS, vol. 1282, pp. 205\u2013219. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63383-9_82"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-45315-6_8","volume-title":"Foundations of Software Science and Computation Structures","author":"N Busi","year":"2001","unstructured":"Busi, N., Gorrieri, R., Zavattaro, G.: Temporary data in shared dataspace coordination languages. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 121\u2013136. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_8"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-46425-5_3","volume-title":"Programming Languages and Systems","author":"N Busi","year":"2000","unstructured":"Busi, N., Zavattaro, G.: On the expressiveness of event notification in data-driven coordination languages. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 41\u201355. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46425-5_3"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/11841197_10","volume-title":"Web Services and Formal Methods","author":"S Carpineti","year":"2006","unstructured":"Carpineti, S., Castagna, G., Laneve, C., Padovani, L.: A formal account of contracts for web services. In: Bravetti, M., N\u00fa\u00f1ez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 148\u2013162. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11841197_10"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Carriero, N., Gelernter, D.: The S\/Net\u2019s Linda kernel (extended abstract). In: Proceedings of 10th ACM Symposium on Operating System Principles, SOSP 1985, p. 160. ACM (1985)","DOI":"10.1145\/323627.323643"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 261\u2013272. ACM (2008)","DOI":"10.1145\/1328897.1328471"},{"issue":"2","key":"2_CR20","first-page":"1","volume":"13","author":"T Chen","year":"2017","unstructured":"Chen, T., Dezani-Ciancaglini, M., Scalas, A., Yoshida, N.: On the preciseness of subtyping in session types. Log. Methods Comput. Sci. 13(2), 1\u201361 (2017)","journal-title":"Log. Methods Comput. Sci."},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-63383-9_83","volume-title":"Coordination Languages and Models","author":"R De Nicola","year":"1997","unstructured":"De Nicola, R., Ferrari, G.L., Pugliese, R.: Coordinating mobile agents via blackboards and access rights. In: Garlan, D., Le M\u00e9tayer, D. (eds.) COORDINATION 1997. LNCS, vol. 1282, pp. 220\u2013237. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63383-9_83"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-61052-9_45","volume-title":"Coordination Languages and Models","author":"R De Nicola","year":"1996","unstructured":"De Nicola, R., Pugliese, R.: A process algebra based on Linda. In: Ciancarini, P., Hankin, C. (eds.) COORDINATION 1996. LNCS, vol. 1061, pp. 160\u2013178. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61052-9_45"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"Automata, Languages and Programming","author":"C Dufourd","year":"1998","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103\u2013115. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055044"},{"issue":"1-2","key":"2_CR24","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-540-27813-9_19","volume-title":"Computer Aided Verification","author":"C Fournet","year":"2004","unstructured":"Fournet, C., Hoare, T., Rajamani, S.K., Rehof, J.: Stuck-free conformance. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 242\u2013254. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_19"},{"issue":"2\u20133","key":"2_CR26","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.: Subtyping for session types in the pi calculus. Acta Informatica 42(2\u20133), 191\u2013225 (2005)","journal-title":"Acta Informatica"},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/2363.2433","volume":"7","author":"D Gelernter","year":"1985","unstructured":"Gelernter, D.: Generative communication in Linda. ACM Trans. Program. Lang. Syst. 7(1), 80\u2013112 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR28","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). https:\/\/doi.org\/10.1007\/BFb0053567"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 273\u2013284. ACM (2008)","DOI":"10.1145\/1328897.1328472"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Jespersen, T.B.L. Munksgaard, P., Larsen, K.F.: Session types for Rust. In: Proceedings of 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, pp. 13\u201322 (2015)","DOI":"10.1145\/2808098.2808100"},{"key":"2_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1844-9","volume-title":"Automata and Computability","author":"D Kozen","year":"1997","unstructured":"Kozen, D.: Automata and Computability. Springer, New York (1997). https:\/\/doi.org\/10.1007\/978-1-4612-1844-9"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-540-74407-8_15","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"C Laneve","year":"2007","unstructured":"Laneve, C., Padovani, L.: The Must preorder revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 212\u2013225. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_15"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-662-54458-7_26","volume-title":"Foundations of Software Science and Computation Structures","author":"J Lange","year":"2017","unstructured":"Lange, J., Yoshida, N.: On the undecidability of asynchronous session subtyping. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 441\u2013457. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_26"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: Proceedings of 9th International Symposium on Haskell, Haskell 2016, pp. 133\u2013145 (2016)","DOI":"10.1145\/2976002.2976018"},{"key":"2_CR35","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Harlow (1989)"},{"key":"2_CR36","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Englewood Cliffs (1967)"},{"key":"2_CR37","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":"2_CR38","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). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_23"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Ng, N., Yoshida, N.: Static deadlock detection for concurrent go by global session graph synthesis. In: Proceedings of 25th International Conference on Compiler Construction, CC 2016, pp. 174\u2013184 (2016)","DOI":"10.1145\/2892208.2892232"},{"key":"2_CR40","unstructured":"OASIS: Web Services Business Process Execution Language Version 2.0 OASIS Standard. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.pdf"},{"issue":"2","key":"2_CR41","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.ic.2006.06.002","volume":"205","author":"A Rensink","year":"2007","unstructured":"Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125\u2013198 (2007)","journal-title":"Inf. Comput."},{"issue":"2","key":"2_CR42","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/321160.321170","volume":"10","author":"JC Shepherdson","year":"1963","unstructured":"Shepherdson, J.C., Sturgis, H.E.: Computability of recursive functions. J. ACM 10(2), 217\u2013255 (1963)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92408-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:27:04Z","timestamp":1654734424000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-92408-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319924076","9783319924083"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92408-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"27 May 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Languages and Models","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/2018.discotec.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}