{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:09:46Z","timestamp":1784232586889,"version":"3.55.0"},"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\n                    <jats:italic toggle=\"yes\">\u03bb<\/jats:italic>\n                    QC, 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.\n                    <jats:italic toggle=\"yes\">\u03bb<\/jats:italic>\n                    QC 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":0,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2518-614X","authenticated-orcid":false,"given":"Andrew K.","family":"Hirsch","sequence":"additional","affiliation":[{"name":"SUNY Buffalo, Buffalo, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Mako Bates Shun Kashiwa Syed Jafri Gan Shen Lindsey Kuper and Joseph P. Near. 2025. Efficient Portable CensusPolymorphic Choreographic Programming. Proc. ACM Program. Lang. 9 PLDI Article 193 (June 2025) 24 pages. doi: 10.1145\/3729296","DOI":"10.1145\/3729296"},{"key":"e_1_3_2_3_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). doi: 10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone Fabrizio Montesi and Carsten Sch\u00fcrmann. 2014. Choreographies Logically. In Concurrency Theory (CONCUR). doi: 10.1007\/978-3-662-44584-6_5","DOI":"10.1007\/978-3-662-44584-6_5"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.356.3"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715615"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe Eva Graversen Lovro Lugovi\u0107 Fabrizio Montesi and Marco Peressotti. 2023. Modular Compilation for Higher-Order Functional Choreographies. In European Conference on Object-Oriented Programming (ECOOP). doi: 10.4230\/LIPIcs.ECOOP.2023.7","DOI":"10.4230\/LIPIcs.ECOOP.2023.7"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe and Fabrizio Montesi. 2017a. A Core Model for Choreographic Programming. In Formal Aspects of Component Software (FACS). doi: 10.1007\/978-3-319-57666-4_3","DOI":"10.1007\/978-3-319-57666-4_3"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe and Fabrizio Montesi. 2017b. Procedural Choreographic Programming. In Formal Techniques for Distributed Objects Components and Systems (FORTE). doi: 10.1007\/978-3-319-60225-7_7","DOI":"10.1007\/978-3-319-60225-7_7"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peresotti. 2018. Communications in Choreographies Revisited. In Symposium on Applied Computing (SAC). doi: 10.1145\/3167132.3167267","DOI":"10.1145\/3167132.3167267"},{"key":"e_1_3_2_11_1","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peresotti. 2021a. Formalizing a Turing-Complete Choreographic Language in Coq. In Interactive Theorem Proving (ITP)."},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000114"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Andrew K. Hirsch and Deepak Garg. 2022. Pirouette: Higher-Order Typed Functional Choreographies. In Principles of Programming Languages (POPL). doi: 10.1145\/3498684","DOI":"10.1145\/3498684"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Stephanie Balzer and Robbert Krebbers. 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. In International Conference on Functional Programming (ICFP). doi: 10.1145\/3547638","DOI":"10.1145\/3547638"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Ivan Lanese Fabrizio Montesi and Gianluigi Zavattaro. 2013. Amending Choreographies. In Workshop on Automated Specification and Verification of Web Systems (WWV). doi: 10.4204\/EPTCS.123.5","DOI":"10.4204\/EPTCS.123.5"},{"key":"e_1_3_2_19_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_3_2_20_1","doi-asserted-by":"publisher","unstructured":"Fabrizio Montesi. 2023. Introduction to Choreographies. Cambridge University Press. doi: 10.1017\/9781108981491","DOI":"10.1017\/9781108981491"},{"key":"e_1_3_2_21_1","doi-asserted-by":"crossref","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.","DOI":"10.1007\/978-3-540-73228-0_23"},{"key":"e_1_3_2_22_1","unstructured":"Benjamin C Pierce. 2002. Types and Programming Languages. Springer."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-815"},{"key":"e_1_3_2_24_1","unstructured":"Ashley Samuelson Andrew K. Hirsch and Ethan Cecchetti. 2025a. Choreographic Quick Changes: First-Class Location (Set) Polymorphism. Technical Report. https:\/\/arxiv.org\/abs\/2506.10913."},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Ashley Samuelson Andrew K. Hirsch and Ethan Cecchetti. 2025b. Choreographic Quick Changes Rocq Proofs. doi: 10.5281\/zenodo.16783266","DOI":"10.5281\/zenodo.16783266"},{"key":"e_1_3_2_26_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_3_2_27_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 ( \u27e8 Programming \u27e9 ). doi: 10.22152\/programming-journal.org\/2023\/7\/14","DOI":"10.22152\/programming-journal.org\/2023\/7\/14"},{"key":"e_1_3_2_28_1","unstructured":"Gaisi Takeuti. 1987. Proof Theory. Dover Books. 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":[[2026,7,16]],"date-time":"2026-07-16T10:06:27Z","timestamp":1784196387000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}