{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:51:42Z","timestamp":1754488302865,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031353604"},{"type":"electronic","value":"9783031353611"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-35361-1_8","type":"book-chapter","created":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T14:04:07Z","timestamp":1686751447000},"page":"144-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Reasoning About Choreographic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7866-7484","authenticated-orcid":false,"given":"Lu\u00eds","family":"Cruz-Filipe","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9430-4907","authenticated-orcid":false,"given":"Eva","family":"Graversen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4666-901X","authenticated-orcid":false,"given":"Fabrizio","family":"Montesi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0243-0480","authenticated-orcid":false,"given":"Marco","family":"Peressotti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,15]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2(3), 359\u2013385 (1980). https:\/\/doi.org\/10.1145\/357103.357110","DOI":"10.1145\/357103.357110"},{"key":"8_CR2","unstructured":"Apt, K.R., Olderog, E.: Fifty years of Hoare\u2019s logic. CoRR abs\/1904.03917 (2019)"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Apt, K.R., Olderog, E.-R., Boer, F.S.: Verification of sequential and concurrent programs, vol. 2. Springer (2009). https:\/\/doi.org\/10.1007\/978-1-84882-745-5","DOI":"10.1007\/978-1-84882-745-5"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-15375-4_12","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Bocchi","year":"2010","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162\u2013176. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12"},{"key":"8_CR5","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. 6269, pp. 222\u2013236. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) Procs. POPL, pp. 263\u2013274. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C.: Choreographies, logically. Distributed Computing 31(1), 51\u201367 (2017). https:\/\/doi.org\/10.1007\/s00446-017-0295-1","DOI":"10.1007\/s00446-017-0295-1"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Graversen, E., Lugovic, L., Montesi, F., Peressotti, M.: Functional choreographic programming. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) Theoretical Aspects of Computing \u2013 ICTAC 2022. ICTAC 2022. Lecture Notes in Computer Science, vol. 13572, pp. 212\u2013237. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_15","DOI":"10.1007\/978-3-031-17715-6_15"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-319-60225-7_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Montesi, F.: Procedural choreographic programming. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 92\u2013107. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-60225-7_7"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.tcs.2019.07.005","volume":"802","author":"L Cruz-Filipe","year":"2020","unstructured":"Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38\u201366 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.07.005","journal-title":"Theor. Comput. Sci."},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-85315-0_8","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2021","author":"L Cruz-Filipe","year":"2021","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: Cerone, A., \u00d6lveczky, P.C. (eds.) ICTAC 2021. LNCS, vol. 12819, pp. 115\u2013133. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_8"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Formalising a Turing-complete choreographic language in Coq. In: Cohen, L., Kaliszyk, C. (eds.) Procs. ITP. LIPIcs, vol. 193, pp. 1\u201318. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.15","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Dalla Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies: theory and implementation. Log. Methods Comput. Sci. 13(2), 1\u201357 (2017). https:\/\/doi.org\/10.23638\/LMCS-13(2:1)2017","DOI":"10.23638\/LMCS-13(2:1)2017"},{"issue":"6","key":"8_CR14","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976). https:\/\/doi.org\/10.1109\/TIT.1976.1055638","journal-title":"IEEE Trans. Inf. Theory"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Gastin, P., Laroussinie, F. (eds.): CONCUR 2010. LNCS, vol. 6269. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4","DOI":"10.1007\/978-3-642-15375-4"},{"key":"8_CR16","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M.: Choreographies as objects. CoRR abs\/2005.09520 (2020), https:\/\/arxiv.org\/abs\/2005.09520"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisenburger, P.: Multiparty languages: the choreographic and multitier cases (pearl). In: M\u00f8ller, A., Sridharan, M. (eds.) Proceedings ECOOP. LIPIcs, vol. 194, pp. 1\u201327. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.22","DOI":"10.4230\/LIPIcs.ECOOP.2021.22"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6(POPL), 1\u201327 (2022). https:\/\/doi.org\/10.1145\/3498684","DOI":"10.1145\/3498684"},{"issue":"10","key":"8_CR19","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Jongmans, S., van den Bos, P.: A predicate transformer for choreographies - computing preconditions in choreographic programming. In: Sergey, I. (eds.) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol. 13240, pp. 520\u2013547. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_19","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Leesatapornwongsa, T., Lukman, J.F., Lu, S., Gunawi, H.S.: Taxdc: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In: Conte, T., Zhou, Y. (eds.) Procs. ASPLOS, pp. 517\u2013530. ACM (2016). https:\/\/doi.org\/10.1145\/2872362.2872374","DOI":"10.1145\/2872362.2872374"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BF00289266","volume":"15","author":"G Levin","year":"1981","unstructured":"Levin, G., Gries, D.: A proof technique for communicating sequential processes. Acta Informatica 15, 281\u2013302 (1981). https:\/\/doi.org\/10.1007\/BF00289266","journal-title":"Acta Informatica"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-39570-8_13","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"HA L\u00f3pez","year":"2016","unstructured":"L\u00f3pez, H.A., Nielson, F., Nielson, H.R.: Enforcing availability in failure-aware communicating systems. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 195\u2013211. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_13"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Melgratti, H.C., Padovani, L.: Chaperone contracts for higher-order sessions. Proc. ACM Program. Lang. 1(ICFP), 1\u201329 (2017). https:\/\/doi.org\/10.1145\/3110279","DOI":"10.1145\/3110279"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Applying \u201cdesign by contract.\u201d Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"8_CR26","unstructured":"Montesi, F.: Choreographic programming, Ph. D. Thesis, IT University of Copenhagen (2013)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023)","DOI":"10.1017\/9781108981491"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-40184-8_30","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"F Montesi","year":"2013","unstructured":"Montesi, F., Yoshida, N.: Compositional choreographies. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 425\u2013439. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_30"},{"issue":"12","key":"8_CR29","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"8_CR30","doi-asserted-by":"publisher","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Schneider-Kamp, P., Hanus, M. (eds.) Procs. PPDP, pp. 161\u2013172. ACM (2011). https:\/\/doi.org\/10.1145\/2003476.2003499","DOI":"10.1145\/2003476.2003499"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Waye, L., Chong, S., Dimoulas, C.: Whip: higher-order contracts for modern services. Proc. ACM Program. Lang. 1(ICFP), 1\u201328 (2017). https:\/\/doi.org\/10.1145\/3110280","DOI":"10.1145\/3110280"}],"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-031-35361-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T14:05:17Z","timestamp":1686751517000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-35361-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031353604","9783031353611"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-35361-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"15 June 2023","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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 June 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2023\/coordination","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}