{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:16:50Z","timestamp":1792264610610,"version":"4.4.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, Pirouette is defined generically over a (local) language of messages, and lifts guarantees about the message type system to its own. Message type soundness also guarantees deadlock freedom. All of our results are verified in Coq.<\/jats:p>","DOI":"10.1145\/3498684","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Pirouette: higher-order typed functional choreographies"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2518-614X","authenticated-orcid":false,"given":"Andrew K.","family":"Hirsch","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/30.5.437"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.041"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429101"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_5"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_12"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599439"},{"key":"e_1_2_2_7_1","unstructured":"Lu\u00eds Cruz-Filipe Eva Graversen Lovro Lugovi\u0107 Fabrizio Montesi and Marco Peressotti. 2021. Choreographies as Functions. arxiv:2111.03701 In Preperation for ECOOP.  Lu\u00eds Cruz-Filipe Eva Graversen Lovro Lugovi\u0107 Fabrizio Montesi and Marco Peressotti. 2021. Choreographies as Functions. arxiv:2111.03701 In Preperation for ECOOP."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57666-4_3"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60225-7_7"},{"key":"e_1_2_2_10_1","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2019. Choreographies in Coq. In Types for Proofs and Programs (TYPES). http:\/\/www.ii.uib.no\/~bezem\/abstracts\/TYPES_2019_paper_27  Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2019. Choreographies in Coq. In Types for Proofs and Programs (TYPES). http:\/\/www.ii.uib.no\/~bezem\/abstracts\/TYPES_2019_paper_27"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2021. Certifying Choreography Compilation. In International Colloquium on Theoretical Aspects of Computing (ICTAC).  Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2021. Certifying Choreography Compilation. In International Colloquium on Theoretical Aspects of Computing (ICTAC).","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"e_1_2_2_12_1","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2021. Formalizing a Turing-Complete Choreographic Language in Coq. In Interactive Theorem Proving (ITP).  Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2021. Formalizing a Turing-Complete Choreographic Language in Coq. In Interactive Theorem Proving (ITP)."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19282-6_5"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2370776.2370794"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.228"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01491213"},{"key":"e_1_2_2_17_1","unstructured":"Saverio Giallorenzo Fabrizio Montesi and Marco Peressotti. 2020. Choreographies as Objects. arxiv:2005.09520  Saverio Giallorenzo Fabrizio Montesi and Marco Peressotti. 2020. Choreographies as Objects. arxiv:2005.09520"},{"key":"e_1_2_2_18_1","volume-title":"Hirsch and Deepak Garg","author":"Andrew","year":"2021","unstructured":"Andrew K. Hirsch and Deepak Garg . 2021 . Pirouette : Higher-Order Typed Functional Choreographies (Technical Report). MPI-SWS. https:\/\/www.mpi-sws.org\/tr\/2021-004.pdf Andrew K. Hirsch and Deepak Garg. 2021. Pirouette: Higher-Order Typed Functional Choreographies (Technical Report). MPI-SWS. https:\/\/www.mpi-sws.org\/tr\/2021-004.pdf"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.123.5"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.34.7"},{"key":"e_1_2_2_23_1","volume-title":"Introduction to Choreographies","author":"Montesi Fabrizio","unstructured":"Fabrizio Montesi . 2020. Introduction to Choreographies . Cambridge University Press . Accepted for Publication. Fabrizio Montesi. 2020. Introduction to Choreographies. Cambridge University Press. Accepted for Publication."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78663-4_9"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3291638"},{"key":"e_1_2_2_26_1","volume-title":"Racket Documentation: Concurrency and Synchronization. https:\/\/docs.racket-lang.org\/guide\/concurrency.html Accessed","author":"Team The Racket","year":"2021","unstructured":"The Racket Team . 2021 . Racket Documentation: Concurrency and Synchronization. https:\/\/docs.racket-lang.org\/guide\/concurrency.html Accessed July 3, 2021. The Racket Team. 2021. Racket Documentation: Concurrency and Synchronization. https:\/\/docs.racket-lang.org\/guide\/concurrency.html Accessed July 3, 2021."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_23"},{"key":"e_1_2_2_28_1","unstructured":"The World Wide Web Consortium (W3C). 2004. WS Choreography Model Overview. https:\/\/www.w3.org\/TR\/ws-chor-model\/ Accessed January 29 2021.  The World Wide Web Consortium (W3C). 2004. WS Choreography Model Overview. https:\/\/www.w3.org\/TR\/ws-chor-model\/ Accessed January 29 2021."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242704"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498684","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498684","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498684"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":29,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498684"],"URL":"https:\/\/doi.org\/10.1145\/3498684","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}