{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:20:59Z","timestamp":1760059259904,"version":"build-2065373602"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n            Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with \u03bb\n            <jats:sub>\n              <jats:italic toggle=\"yes\">QC<\/jats:italic>\n            <\/jats:sub>\n            , the first typed choreographic language with\n            <jats:italic toggle=\"yes\">first class process names<\/jats:italic>\n            and polymorphism over both types and (sets of) locations. \u03bb\n            <jats:sub>\n              <jats:italic toggle=\"yes\">QC<\/jats:italic>\n            <\/jats:sub>\n            also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.\n          <\/jats:p>","DOI":"10.1145\/3763114","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1783-1808","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Choreographic Quick Changes: First-Class Location (Set) Polymorphism"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-8800-2590","authenticated-orcid":false,"given":"Ashley","family":"Samuelson","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2518-614X","authenticated-orcid":false,"given":"Andrew K.","family":"Hirsch","sequence":"additional","affiliation":[{"name":"SUNY Buffalo, Buffalo, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7900-8328","authenticated-orcid":false,"given":"Ethan","family":"Cecchetti","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729296"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone and Fabrizio Montesi. 2013. Deadlock-Freedom-by-Design: Multiparty Asynchronous Global Programming. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2429069.2429101 10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone Fabrizio Montesi and Carsten Sch\u00fcrmann. 2014. Choreographies Logically. In Concurrency Theory (CONCUR). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_5 10.1007\/978-3-662-44584-6_5","DOI":"10.1007\/978-3-662-44584-6_5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.356.3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715-6_15"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe and Fabrizio Montesi. 2017. A Core Model for Choreographic Programming. In Formal Aspects of Component Software (FACS). https:\/\/doi.org\/10.1007\/978-3-319-57666-4_3 10.1007\/978-3-319-57666-4_3","DOI":"10.1007\/978-3-319-57666-4_3"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe and Fabrizio Montesi. 2017. Procedural Choreographic Programming. In Formal Techniques for Distributed Objects Components and Systems (FORTE). https:\/\/doi.org\/10.1007\/978-3-319-60225-7_7 10.1007\/978-3-319-60225-7_7","DOI":"10.1007\/978-3-319-60225-7_7"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167132.3167267"},{"key":"e_1_2_1_10_1","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peresotti. 2021. Formalizing a Turing-Complete Choreographic Language in Coq. In Interactive Theorem Proving (ITP)."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000114"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547638"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.123.5"},{"volume-title":"Choreographic Programming. Ph. D. Dissertation","author":"Montesi Fabrizio","key":"e_1_2_1_18_1","unstructured":"Fabrizio Montesi. 2013. Choreographic Programming. Ph. D. Dissertation. IT University of Copenhagen. https:\/\/www.fabriziomontesi.com\/files\/choreographic_programming.pdf"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491"},{"volume-title":"Two Session Typing Systems for Higher-Order Mobile Processes","author":"Mostrous Dimitris","key":"e_1_2_1_20_1","unstructured":"Dimitris Mostrous and Nobuko Yoshida. 2007. Two Session Typing Systems for Higher-Order Mobile Processes. In Typed Lambda Calculi and Applications, Simona Ronchi Della Rocca (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 321\u2013335. isbn:978-3-540-73228-0"},{"volume-title":"Types and Programming Languages","author":"Pierce Benjamin C","key":"e_1_2_1_21_1","unstructured":"Benjamin C Pierce. 2002. Types and Programming Languages. Springer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_15"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Ashley Samuelson Andrew K. Hirsch and Ethan Cecchetti. 2025. Choreographic Quick Changes: First-Class Location (Set) Polymorphism. arxiv:2506.10913","DOI":"10.1145\/3763114"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Ashley Samuelson Andrew K. Hirsch and Ethan Cecchetti. 2025. Choreographic Quick Changes Rocq Proofs. https:\/\/doi.org\/10.5281\/zenodo.16783266 10.5281\/zenodo.16783266","DOI":"10.5281\/zenodo.16783266"},{"key":"e_1_2_1_25_1","unstructured":"Davide Sangiorgi. 1993. Expressing mobility in process algebras: first-order and higher-order paradigms. Ph. D. Dissertation. http:\/\/hdl.handle.net\/1842\/6569"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Ian Sweet David Darais David Heath Ryan Estes William Harris and Michael Hicks. 2023. Symphony: Expressive Secure Multiparty Computation with Coordination. In The Art Science and Engineering of Programming (langle Programmingrangle ). https:\/\/doi.org\/10.22152\/programming-journal.org\/2023\/7\/14 10.22152\/programming-journal.org\/2023\/7\/14","DOI":"10.22152\/programming-journal.org\/2023\/7\/14"},{"key":"e_1_2_1_27_1","volume-title":"Proof Theory","author":"Takeuti Gaisi","year":"2013","unstructured":"Gaisi Takeuti. 1987. Proof Theory. Dover Books. isbn:0-486-49073-4 Second Edition, republished by Dover Books in 2013. Originally published by North-Holland, Amsterdam"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763114","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:47:05Z","timestamp":1760032025000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":27,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763114"],"URL":"https:\/\/doi.org\/10.1145\/3763114","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}