{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T01:27:16Z","timestamp":1778635636108,"version":"3.51.4"},"reference-count":76,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"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,8,29]]},"abstract":"<jats:p>Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming.  \nChannel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along channels.  \nRepresentatives of the GV (Wadler's \"Good Variation\") session type family are of particular appeal because they not only assert session fidelity but also deadlock freedom, inspired by a Curry-Howard correspondence to linear logic.  \nA restriction of current versions of GV, however, is the focus on binary sessions, limiting concurrent interactions within a session to two participants.  \nThis paper introduces Multiparty GV (MPGV), a functional language with multiparty session types, allowing concurrent interactions among several participants.  \nMPGV upholds the strong guarantees of its ancestor GV, including deadlock freedom, despite session interleaving and delegation.  \nMPGV has a novel redirecting construct for modular programming with first-class endpoints,  \nthanks to which we give a type-preserving translation from binary session types to MPGV to show that MPGV is strictly more general than binary GV.  \nAll results in this paper have been mechanized using the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3547638","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"466-495","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Multiparty GV: functional multiparty session types with certified deadlock freedom"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8347-3529","authenticated-orcid":false,"given":"Stephanie","family":"Balzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531058"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.30"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.33"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.412"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.22"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414109"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38493-6_4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000188"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301641"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_20"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926435"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.36"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290341"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.314.3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434297"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000231"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2018.08.005"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.69.6"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498662"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6884760"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808100"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_14"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614941"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3171"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.004"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.304.4"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3471874.3472979"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78089-0_6"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290337"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976018"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_1_56_1","unstructured":"Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools. https:\/\/homepages.inf.ed.ac.uk\/slindley\/papers\/fst.pdf \t\t\t\t  Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools. https:\/\/homepages.inf.ed.ac.uk\/slindley\/papers\/fst.pdf"},{"key":"e_1_2_1_57_1","unstructured":"Fabrizio Montesi. 2020. Introduction to Choreographies. https:\/\/www.fabriziomontesi.com\/teaching\/ct-2020\/files\/chor-notes.pdf Draft \t\t\t\t  Fabrizio Montesi. 2020. Introduction to Choreographies. https:\/\/www.fabriziomontesi.com\/teaching\/ct-2020\/files\/chor-notes.pdf Draft"},{"key":"e_1_2_1_58_1","volume-title":"abs\/1803.01049","author":"Montesi Fabrizio","year":"2018","unstructured":"Fabrizio Montesi and Marco Peressotti . 2018. Classical Transitions . CoRR , abs\/1803.01049 ( 2018 ), arxiv:1803.01049. arxiv:1803.01049 Fabrizio Montesi and Marco Peressotti. 2018. Classical Transitions. CoRR, abs\/1803.01049 (2018), arxiv:1803.01049. arxiv:1803.01049"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000289"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411290"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.21"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_2_1_69_1","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited (technical report). https:\/\/www.doc.ic.ac.uk\/research\/technicalreports\/2018\/DTRS18-6.pdf \t\t\t\t  Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited (technical report). https:\/\/www.doc.ic.ac.uk\/research\/technicalreports\/2018\/DTRS18-6.pdf"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354184"},{"key":"e_1_2_1_72_1","volume-title":"A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation","author":"Toninho Bernardo","unstructured":"Bernardo Toninho . 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation . Carnegie Mellon University and New University of Lisbon . Bernardo Toninho. 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation. Carnegie Mellon University and New University of Lisbon."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242173"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78089-0_9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":76,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547638"],"URL":"https:\/\/doi.org\/10.1145\/3547638","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}