{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T21:15:51Z","timestamp":1775769351691,"version":"3.50.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/Y00339X\/1"],"award-info":[{"award-number":["EP\/Y00339X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/T014512\/1"],"award-info":[{"award-number":["EP\/T014512\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Multiparty session types (MPST) provide a rigorous foundation for verifying the safety and liveness of concurrent systems. However, existing approaches often force a difficult trade-off: classical, projection-based techniques are compositional but limited in expressiveness, while more recent techniques achieve higher expressiveness by relying on non-compositional, whole-system model checking, which scales poorly.<\/jats:p>\n                  <jats:p>This paper introduces a new approach to MPST that delivers both expressiveness and compositionality, called the synthetic approach. Our key innovation is a type system that verifies each process directly against a global protocol specification, represented as a labelled transition system (LTS) in general, with global types as a special case. This approach uniquely avoids the need for intermediate local types and projection.<\/jats:p>\n                  <jats:p>We demonstrate that our approach, while conceptually simpler, supports a benchmark of challenging protocols that were previously beyond the reach of compositional techniques in the MPST literature. We generalise our type system, showing that it can validate processes against any specification that constitutes a \"well-behaved\" LTS, supporting protocols not expressible with the standard global type syntax. The entire framework, including all theorems and many examples, has been formalised and mechanised in Agda, and we have developed a prototype implementation as an extension to VS Code.<\/jats:p>","DOI":"10.1145\/3776692","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1442-1470","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Synthetic Reconstruction of Multiparty Session Types"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6939-4189","authenticated-orcid":false,"given":"David","family":"Castro-Perez","sequence":"first","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8494-7696","authenticated-orcid":false,"given":"Francisco","family":"Ferreira","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, Egham, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4394-8745","authenticated-orcid":false,"given":"Sung-Shik","family":"Jongmans","sequence":"additional","affiliation":[{"name":"University of Groningen, Groningen, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_2_1_2_1","volume-title":"COORDINATION (LNCS","volume":"106","author":"Barbanera Franco","year":"2020","unstructured":"Franco Barbanera, Ivan Lanese, and Emilio Tuosto. 2020. Choreography Automata. In COORDINATION (LNCS, Vol. 12134). Springer, 86\u2013106. https:\/\/doi.org\/10.1007\/978-3-030-50029-0_6 10.1007\/978-3-030-50029-0_6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf00257484"},{"key":"e_1_2_1_4_1","volume-title":"Meeting Deadlines Together. In CONCUR (LIPIcs","volume":"296","author":"Bocchi Laura","year":"2015","unstructured":"Laura Bocchi, Julien Lange, and Nobuko Yoshida. 2015. Meeting Deadlines Together. In CONCUR (LIPIcs, Vol. 42). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 283\u2013296. https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2015.283 10.4230\/LIPICS.CONCUR.2015.283"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.356.2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"David Castro-Perez Francisco Ferreira Lorenzo Gheri and Nobuko Yoshida. 2021. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In PLDI. ACM 237\u2013251. https:\/\/doi.org\/10.1145\/3453483.3454041 10.1145\/3453483.3454041","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2511.22692"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"David Castro-Perez Sung-Shik Jongmans and Francisco Ferreira Ruiz. 2025. A Synthetic Reconstruction of Multiparty Session Types (Software Artifact). https:\/\/doi.org\/10.5281\/zenodo.17741396 10.5281\/zenodo.17741396","DOI":"10.5281\/zenodo.17741396"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2022.8"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2018.12.002"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_15"},{"key":"e_1_2_1_14_1","volume-title":"Language-Games and Information: Kantian Themes in the Philosophy of Logic.","author":"Hintikka Jaakko","unstructured":"Jaakko Hintikka. 1973. Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic. Oxford, England: Oxford, Clarendon Press."},{"key":"e_1_2_1_15_1","volume-title":"CONCUR (Lecture Notes in Computer Science","volume":"523","author":"Honda Kohei","year":"1993","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR (Lecture Notes in Computer Science, Vol. 715). Springer, 509\u2013523. https:\/\/doi.org\/10.1007\/3-540-57208-2_35 10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0053567"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL. ACM 273\u2013284. https:\/\/doi.org\/10.1145\/1328438.1328472 10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_1_19_1","volume-title":"Proc. ACM Program. Lang., 6, POPL","author":"Jacobs Jules","year":"2022","unstructured":"Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022. Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang., 6, POPL (2022), 1\u201333. https:\/\/doi.org\/10.1145\/3498662 10.1145\/3498662"},{"key":"e_1_2_1_20_1","volume-title":"Proc. ACM Program. Lang., 6, ICFP","author":"Jacobs Jules","year":"2022","unstructured":"Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang., 6, ICFP (2022), 466\u2013495. https:\/\/doi.org\/10.1145\/3547638 10.1145\/3547638"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.42"},{"key":"e_1_2_1_22_1","volume-title":"ESOP (LNCS","volume":"279","author":"Jongmans Sung-Shik","unstructured":"Sung-Shik Jongmans and N. Yoshida. 2020. Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types. In ESOP (LNCS, Vol. 12075). Springer, 251\u2013279. https:\/\/doi.org\/10.1007\/978-3-030-44914-8_10 10.1007\/978-3-030-44914-8_10"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SCAM.2009.28"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Julien Lange Emilio Tuosto and Nobuko Yoshida. 2015. From Communicating Machines to Graphical Choreographies. In POPL. ACM 221\u2013232. https:\/\/doi.org\/10.1145\/2676726.2676964 10.1145\/2676726.2676964","DOI":"10.1145\/2676726.2676964"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2025.15"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814302"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Robin Milner. 1982. Four Combinators for Concurrency. In PODC. ACM 104\u2013110. https:\/\/doi.org\/10.1145\/800220.806687 10.1145\/800220.806687","DOI":"10.1145\/800220.806687"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662085"},{"key":"e_1_2_1_31_1","volume-title":"Proc. ACM Program. Lang., 3, POPL","author":"Scalas Alceste","year":"2019","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3, POPL (2019), 30:1\u201330:29. https:\/\/doi.org\/10.1145\/3290343 10.1145\/3290343"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2023.28"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2025.31"},{"key":"e_1_2_1_34_1","volume-title":"Proc. ACM Program. Lang., 9, POPL","author":"Udomsrirungruang Thien","year":"2025","unstructured":"Thien Udomsrirungruang and Nobuko Yoshida. 2025. Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types. Proc. ACM Program. Lang., 9, POPL (2025), 1040\u20131071. https:\/\/doi.org\/10.1145\/3704872 10.1145\/3704872"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611013"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470531"},{"key":"e_1_2_1_37_1","volume-title":"ICDCIT (LNCS","volume":"93","author":"Yoshida Nobuko","year":"2020","unstructured":"Nobuko Yoshida and Lorenzo Gheri. 2020. A Very Gentle Introduction to Multiparty Session Types. In ICDCIT (LNCS, Vol. 11969). Springer, 73\u201393. https:\/\/doi.org\/10.1007\/978-3-030-36987-3_5 10.1007\/978-3-030-36987-3_5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776692","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:47Z","timestamp":1767898787000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776692"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776692"],"URL":"https:\/\/doi.org\/10.1145\/3776692","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}