{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T04:44:53Z","timestamp":1778215493922,"version":"3.51.4"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031911200","type":"print"},{"value":"9783031911217","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Choreographic programming (CP) is a method to implement distributed systems that ensures communication deadlock freedom by design. To use CP, though, the number of processes and the network among them must be known statically. Often, that information is known only dynamically. Thus, existing CP languages cannot be used to implement <jats:italic>process-parametric<\/jats:italic> distributed systems.\n<\/jats:p>\n          <jats:p>This paper introduces <jats:italic>first-person<\/jats:italic> choreographic programming (1CP) to support the implementation of process-parametric distributed systems while also ensuring communication deadlock freedom. We present both a design of 1CP (new calculus, formalised in Isabelle\/HOL) and an implementation (new language and tooling, integrated in VS Code).<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_3","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:50:18Z","timestamp":1746190218000},"page":"62-90","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["First-Person Choreographic Programming with Continuation-Passing Communications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4394-8745","authenticated-orcid":false,"given":"Sung-Shik","family":"Jongmans","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Apt, K.R., de\u00a0Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science, Springer (2009)","DOI":"10.1007\/978-1-84882-745-5"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Carbone, M., Cruz-Filipe, L., Montesi, F., Murawska, A.: Multiparty classical choreographies. In: LOPSTR. Lecture Notes in Computer Science, vol. 11408, pp. 59\u201376. Springer (2018)","DOI":"10.1007\/978-3-030-13838-7_4"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: ESOP. Lecture Notes in Computer Science, vol.\u00a04421, pp. 2\u201317. Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_2"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1\u20138:78 (2012)","DOI":"10.1145\/2220365.2220367"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL. pp. 263\u2013274. ACM (2013)","DOI":"10.1145\/2429069.2429101"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C.: Choreographies, logically. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a08704, pp. 47\u201362. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_5"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Carbone, M., Montesi, F., Sch\u00fcrmann, C.: Choreographies, logically. Distributed Comput. 31(1), 51\u201367 (2018)","DOI":"10.1007\/s00446-017-0295-1"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Castro, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures. PACMPL 3(POPL), 29:1\u201329:30 (2019)","DOI":"10.1145\/3290342"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Castro-Perez, D., Ferreira, F., Gheri, L., Yoshida, N.: Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In: PLDI. pp. 237\u2013251. ACM (2021)","DOI":"10.1145\/3453483.3454041"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Castro-Perez, D., Ferreira, F., Yoshida, N.: EMTST: engineering the meta-theory of session types. In: TACAS (2). Lecture Notes in Computer Science, vol. 12079, pp. 278\u2013285. Springer (2020)","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Chang, E.J.H., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979)","DOI":"10.1145\/359104.359108"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Coto, A., Guanciale, R., Tuosto, E.: An abstract framework for choreographic testing. J. Log. Algebraic Methods Program. 123, 100712 (2021)","DOI":"10.1016\/j.jlamp.2021.100712"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Graversen, E., Montesi, F., Peressotti, M.: Reasoning about choreographic programs. In: COORDINATION. Lecture Notes in Computer Science, vol. 13908, pp. 144\u2013162. Springer (2023)","DOI":"10.1007\/978-3-031-35361-1_8"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: FoSSaCS. Lecture Notes in Computer Science, vol. 10203, pp. 424\u2013440 (2017)","DOI":"10.1007\/978-3-662-54458-7_25"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Lugovic, L., Montesi, F.: Certified compilation of choreographies with hacc. In: FORTE. Lecture Notes in Computer Science, vol. 13910, pp. 29\u201336. Springer (2023)","DOI":"10.1007\/978-3-031-35355-0_3"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38\u201366 (2020)","DOI":"10.1016\/j.tcs.2019.07.005"},{"key":"3_CR17","unstructured":"Cruz-Filipe, L., Montesi, F.: Now it compiles! certified automatic repair of uncompilable protocols. In: ITP. LIPIcs, vol.\u00a0268, pp. 11:1\u201311:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: ICTAC. Lecture Notes in Computer Science, vol. 12819, pp. 115\u2013133. Springer (2021)","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"3_CR19","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: Formalising a turing-complete choreographic language in coq. In: ITP. LIPIcs, vol.\u00a0193, pp. 15:1\u201315:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Montesi, F., Peressotti, M.: A formal theory of choreographic programming. J. Autom. Reason. 67(2), \u00a021 (2023)","DOI":"10.1007\/s10817-023-09665-3"},{"key":"3_CR21","unstructured":"de\u2019Liguoro, U., Padovani, L.: Mailbox types for unordered interactions. In: ECOOP. LIPIcs, vol.\u00a0109, pp. 15:1\u201315:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2018)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Fokkink, W.: Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series, Springer (2000)","DOI":"10.1007\/978-3-662-04293-9"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Fowler, S., Attard, D.P., Sowul, F., Gay, S.J., Trinder, P.: Special delivery: Programming with mailbox types. Proc. ACM Program. Lang. 7(ICFP), 78\u2013107 (2023)","DOI":"10.1145\/3607832"},{"key":"3_CR24","unstructured":"Fowler, S., Lindley, S., Wadler, P.: Mixing metaphors: Actors as channels and channels as actors. In: ECOOP. LIPIcs, vol.\u00a074, pp. 11:1\u201311:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M.: Choral: Object-oriented choreographic programming. ACM Trans. Program. Lang. Syst. 46(1), 1:1\u20131:59 (2024)","DOI":"10.1145\/3632398"},{"key":"3_CR26","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisenburger, P.: Multiparty languages: The choreographic and multitier cases (pearl). In: ECOOP. LIPIcs, vol.\u00a0194, pp. 22:1\u201322:27. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Hamers, R., Jongmans, S.: Discourje: Runtime verification of communication protocols in clojure. In: TACAS (1). Lecture Notes in Computer Science, vol. 12078, pp. 266\u2013284. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_15"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4(POPL), 6:1\u20136:30 (2020)","DOI":"10.1145\/3371074"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6(POPL), 1\u201327 (2022)","DOI":"10.1145\/3498684"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL. pp. 273\u2013284. ACM (2008)","DOI":"10.1145\/1328897.1328472"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: FASE. Lecture Notes in Computer Science, vol.\u00a09633, pp. 401\u2013418. Springer (2016)","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: FASE. Lecture Notes in Computer Science, vol. 10202, pp. 116\u2013133. Springer (2017)","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Jacobs, J., Balzer, S., Krebbers, R.: Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6(ICFP), 466\u2013495 (2022)","DOI":"10.1145\/3547638"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Jongmans, S.: Discourje: Run-time verification of communication protocols in clojure - live at last. In: FM (2). Lecture Notes in Computer Science, vol. 14934, pp. 158\u2013166. Springer (2024)","DOI":"10.1007\/978-3-031-71177-0_11"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Jongmans, S.: First-person choreographic programming with continuation-passing communications (artifact) (2025), https:\/\/doi.org\/10.5281\/zenodo.14624355","DOI":"10.1007\/978-3-031-91121-7_3"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Jongmans, S., van\u00a0den Bos, P.: A predicate transformer for choreographies - computing preconditions in choreographic programming. In: ESOP. Lecture Notes in Computer Science, vol. 13240, pp. 520\u2013547. Springer (2022)","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: Haskell. pp. 94\u2013105. ACM (2015)","DOI":"10.1145\/2804302.2804319"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Klint, P., van\u00a0der Storm, T., Vinju, J.J.: EASY meta-programming with rascal. In: GTTSE. Lecture Notes in Computer Science, vol.\u00a06491, pp. 222\u2013289. Springer (2009)","DOI":"10.1007\/978-3-642-18023-1_6"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023)","DOI":"10.1017\/9781108981491"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Montesi, F., Yoshida, N.: Compositional choreographies. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a08052, pp. 425\u2013439. Springer (2013)","DOI":"10.1007\/978-3-642-40184-8_30"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Ng, N., Yoshida, N.: Pabble: parameterised scribble. Service Oriented Computing and Applications 9(3-4), 269\u2013284 (2015)","DOI":"10.1007\/s11761-014-0172-8"},{"key":"3_CR42","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)"},{"key":"3_CR43","unstructured":"Plyukhin, D., Peressotti, M., Montesi, F.: Ozone: Fully out-of-order choreographies. In: ECOOP. LIPIcs, vol.\u00a0313, pp. 31:1\u201331:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"3_CR44","unstructured":"Pohjola, J.\u00c5., G\u00f3mez-Londo\u00f1o, A., Shaker, J., Norrish, M.: Kalas: A verified, end-to-end compiler for a choreographic language. In: ITP. LIPIcs, vol.\u00a0237, pp. 27:1\u201327:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Preda, M.D., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies - safe runtime updates of distributed applications. In: COORDINATION. Lecture Notes in Computer Science, vol.\u00a09037, pp. 67\u201382. Springer (2015)","DOI":"10.1007\/978-3-319-19282-6_5"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Preda, M.D., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci. 13(2) (2017)","DOI":"10.23638\/LMCS-13(2:1)2017"},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Preda, M.D., Giallorenzo, S., Lanese, I., Mauro, J., Gabbrielli, M.: AIOCJ: A choreographic framework for safe adaptive distributed applications. In: SLE. Lecture Notes in Computer Science, vol.\u00a08706, pp. 161\u2013170. Springer (2014)","DOI":"10.1007\/978-3-319-11245-9_9"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Scalas, A., Yoshida, N., Benussi, E.: Verifying message-passing programs with dependent behavioural types. In: PLDI. pp. 502\u2013516. ACM (2019)","DOI":"10.1145\/3314221.3322484"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Segall, A.: Distributed network protocols. IEEE Trans. Inf. Theory 29(1), 23\u201334 (1983)","DOI":"10.1109\/TIT.1983.1056620"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Shen, G., Kashiwa, S., Kuper, L.: Haschor: Functional choreographic programming for all (functional pearl). Proc. ACM Program. Lang. 7(ICFP), 541\u2013565 (2023)","DOI":"10.1145\/3607849"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Deni\u00e9lou, P., Bejleri, A., Hu, R.: Parameterised multiparty session types. In: FoSSaCS. Lecture Notes in Computer Science, vol.\u00a06014, pp. 128\u2013145. Springer (2010)","DOI":"10.1007\/978-3-642-12032-9_10"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:41:50Z","timestamp":1746520910000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}