{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:04:18Z","timestamp":1762459458761,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,3,10]],"date-time":"2017-03-10T00:00:00Z","timestamp":1489104000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Danish Council for Free Research","award":["DFF\u20134005-00304"],"award-info":[{"award-number":["DFF\u20134005-00304"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s00446-017-0295-1","type":"journal-article","created":{"date-parts":[[2017,3,10]],"date-time":"2017-03-10T06:22:37Z","timestamp":1489126957000},"page":"51-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Choreographies, logically"],"prefix":"10.1007","volume":"31","author":[{"given":"Marco","family":"Carbone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4666-901X","authenticated-orcid":false,"given":"Fabrizio","family":"Montesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Sch\u00fcrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,10]]},"reference":[{"key":"295_CR1","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","volume":"4","author":"A Avron","year":"1991","unstructured":"Avron, A.: Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell. 4, 225\u2013248 (1991)","journal-title":"Ann. Math. Artif. Intell."},{"key":"295_CR2","doi-asserted-by":"crossref","unstructured":"Basu, S., Bultan, T.: Choreography conformance via synchronizability. In: WWW, pp. 795\u2013804 (2011)","DOI":"10.1145\/1963405.1963516"},{"key":"295_CR3","doi-asserted-by":"crossref","unstructured":"Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL, pp. 191\u2013202 (2012)","DOI":"10.1145\/2103656.2103680"},{"key":"295_CR4","unstructured":"Bellin, G., Scott, P.J.: On the pi-calculus and linear logic. Theor. Comput. Sci. 135(1), 11\u201365 (1994)"},{"key":"295_CR5","doi-asserted-by":"crossref","unstructured":"Bettini, L., Coppo, M., D\u2019Antoni, L., Luca, M.D., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: CONCUR. LNCS, vol. 5201, pp. 418\u2013433. Springer (2008)","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"295_CR6","unstructured":"Business Process Model and Notation. http:\/\/www.omg.org\/spec\/BPMN\/2.0\/"},{"key":"295_CR7","doi-asserted-by":"crossref","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: CONCUR, pp. 222\u2013236 (2010)","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"295_CR8","doi-asserted-by":"crossref","unstructured":"Caires, L., Vieira, H.T.: Conversation types. In: ESOP\u201909. LNCS, vol. 5502, pp. 285\u2013300. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-00590-9_21"},{"issue":"2","key":"295_CR9","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/2220365.2220367","volume":"34","author":"M Carbone","year":"2012","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM TOPLAS 34(2), 8 (2012)","journal-title":"ACM TOPLAS"},{"key":"295_CR10","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL, pp. 263\u2013274 (2013)","DOI":"10.1145\/2429069.2429101"},{"key":"295_CR11","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: FoSSaCS, LNCS. Springer (2017) (accepted for publication)","DOI":"10.1007\/978-3-662-54458-7_25"},{"key":"295_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"295_CR13","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: ESOP\u201998. LNCS, vol. 1381, pp. 22\u2013138. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0053567"},{"key":"295_CR14","doi-asserted-by":"crossref","unstructured":"Lanese, I., Guidi, C., Montesi, F., Zavattaro, G.: Bridging the gap between interaction- and process-oriented choreographies. In: Proceedings of SEFM, pp. 323\u2013332. IEEE (2008)","DOI":"10.1109\/SEFM.2008.11"},{"key":"295_CR15","doi-asserted-by":"crossref","unstructured":"Lange, J., Tuosto, E.: Synthesising choreographies from local session types. In: CONCUR, pp. 225\u2013239 (2012)","DOI":"10.1007\/978-3-642-32940-1_17"},{"key":"295_CR16","unstructured":"Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: Proceedings of POPL 2015, pp. 221\u2013232 (2015). http:\/\/doi.acm.org\/10.1145\/2676726.2676964"},{"key":"295_CR17","unstructured":"Montesi, F.: Choreographic Programming. Ph.D. thesis, IT University of Copenhagen (2013). http:\/\/www.fabriziomontesi.com\/files\/choreographic_programming.pdf"},{"key":"295_CR18","doi-asserted-by":"crossref","unstructured":"Montesi, F., Yoshida, N.: Compositional choreographies. In: CONCUR, pp. 425\u2013439 (2013)","DOI":"10.1007\/978-3-642-40184-8_30"},{"key":"295_CR19","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations for session-based concurrency. In: ESOP, pp. 539\u2013558 (2012)","DOI":"10.1007\/978-3-642-28869-2_27"},{"key":"295_CR20","first-page":"900","volume":"48","author":"G Pottinger","year":"1983","unstructured":"Pottinger, G.: Uniform cut-free formulations of T, S4 and S5 (abstract). J. Symb. Log. 48, 900 (1983)","journal-title":"J. Symb. Log."},{"key":"295_CR21","doi-asserted-by":"crossref","unstructured":"Qiu, Z., Zhao, X., Cai, C., Yang, H.: Towards the theoretical foundation of choreography. In: WWW, pp. 973\u2013982. IEEE (2007)","DOI":"10.1145\/1242572.1242704"},{"issue":"1&2","key":"295_CR22","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(96)00075-8","volume":"167","author":"D Sangiorgi","year":"1996","unstructured":"Sangiorgi, D.: pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. 167(1&2), 235\u2013274 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"295_CR23","volume-title":"The $$\\pi $$ \u03c0 -Calculus: A Theory of Mobil","author":"D Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The $$\\pi $$ \u03c0 -Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"295_CR24","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: ESOP, pp. 350\u2013369 (2013)","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"295_CR25","unstructured":"W3C WS-CDL Working Group: Web services choreography description language version 1.0. http:\/\/www.w3.org\/TR\/2004\/WD-ws-cdl-10-20040427\/ (2004)"},{"issue":"2\u20133","key":"295_CR26","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1017\/S095679681400001X","volume":"24","author":"P Wadler","year":"2014","unstructured":"Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2\u20133), 384\u2013418 (2014). doi: 10.1017\/S095679681400001X","journal-title":"J. Funct. Program."}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00446-017-0295-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-017-0295-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-017-0295-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T11:34:47Z","timestamp":1568892887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00446-017-0295-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,10]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["295"],"URL":"https:\/\/doi.org\/10.1007\/s00446-017-0295-1","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"type":"print","value":"0178-2770"},{"type":"electronic","value":"1432-0452"}],"subject":[],"published":{"date-parts":[[2017,3,10]]}}}