{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:04:21Z","timestamp":1781172261299,"version":"3.54.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["830929"],"award-info":[{"award-number":["830929"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["CA15123,IC1201"],"award-info":[{"award-number":["CA15123,IC1201"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T006544\/1, EP\/K011715\/1, EP\/K034413\/1,EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1, EP\/T006544\/1, EP\/T014709\/1, EP\/V000462\/1, VeTSS"],"award-info":[{"award-number":["EP\/T006544\/1, EP\/K011715\/1, EP\/K034413\/1,EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1, EP\/T006544\/1, EP\/T014709\/1, EP\/V000462\/1, VeTSS"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100016047","name":"Science Fund of the Republic of Serbia","doi-asserted-by":"publisher","award":["6526707"],"award-info":[{"award-number":["6526707"]}],"id":[{"id":"10.13039\/501100016047","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>\n            Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol)\n            <jats:italic>T<\/jats:italic>\n            can be safely used whenever a process implementing one of its supertypes\n            <jats:italic>T<\/jats:italic>\n            \u2032 is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever\n            <jats:italic>T<\/jats:italic>\n            <jats:italic>T<\/jats:italic>\n            \u2032 holds, it is safe to replace an implementation of\n            <jats:italic>T<\/jats:italic>\n            \u2032 with an implementation of the subtype\n            <jats:italic>T<\/jats:italic>\n            , which may allow for more optimised communication patterns.\n          <\/jats:p>\n          <jats:p>\n            We present the first formalisation of the\n            <jats:italic>precise<\/jats:italic>\n            subtyping relation for\n            <jats:italic>asynchronous multiparty<\/jats:italic>\n            sessions. We show that our subtyping relation is\n            <jats:italic>sound<\/jats:italic>\n            (i.e., guarantees safe process replacement, as outlined above) and also\n            <jats:italic>complete<\/jats:italic>\n            : any extension of the relation is unsound. To achieve our results, we develop a novel\n            <jats:italic>session decomposition<\/jats:italic>\n            technique, from\n            <jats:italic>full<\/jats:italic>\n            session types (including internal\/external choices) into\n            <jats:italic>single input\/output session trees<\/jats:italic>\n            (without choices).\n          <\/jats:p>\n          <jats:p>\n            Previous work studies precise subtyping for\n            <jats:italic>binary<\/jats:italic>\n            sessions (with just two participants), or multiparty sessions (with any number of participants) and\n            <jats:italic>synchronous<\/jats:italic>\n            interaction. Here, we cover\n            <jats:italic>multiparty<\/jats:italic>\n            sessions with\n            <jats:italic>asynchronous<\/jats:italic>\n            interaction, where messages are transmitted via FIFO queues (as in the TCP\/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture\n            <jats:italic>all<\/jats:italic>\n            such valid permutations \u2014 and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input\/output trees, and providing a simple reasoning principle for asynchronous message optimisations.\n          <\/jats:p>","DOI":"10.1145\/3434297","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Precise subtyping for asynchronous multiparty sessions"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2253-8285","authenticated-orcid":false,"given":"Silvia","family":"Ghilezan","sequence":"first","affiliation":[{"name":"University of Novi Sad, Serbia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3974-5064","authenticated-orcid":false,"given":"Jovanka","family":"Pantovi\u0107","sequence":"additional","affiliation":[{"name":"University of Novi Sad, Serbia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5420-1527","authenticated-orcid":false,"given":"Ivan","family":"Proki\u0107","sequence":"additional","affiliation":[{"name":"University of Novi Sad, Serbia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1153-6164","authenticated-orcid":false,"given":"Alceste","family":"Scalas","sequence":"additional","affiliation":[{"name":"DTU, Denmark \/ Aston University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3925-8557","authenticated-orcid":false,"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"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.4230\/LIPIcs.CONCUR.2019.38"},{"key":"e_1_2_1_7_1","volume-title":"A Sound Algorithm for Asynchronous Session Subtyping (extended version). Extended version of [Bravetti et al. 2019a], available at: http:\/\/arxiv.org\/abs\/","author":"Bravetti Mario","year":"1907","unstructured":"Mario Bravetti , Marco Carbone , Julien Lange , Nobuko Yoshida , and Gianluigi Zavattaro . 2019b. A Sound Algorithm for Asynchronous Session Subtyping (extended version). Extended version of [Bravetti et al. 2019a], available at: http:\/\/arxiv.org\/abs\/ 1907 .00421. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. 2019b. A Sound Algorithm for Asynchronous Session Subtyping (extended version). Extended version of [Bravetti et al. 2019a], available at: http:\/\/arxiv.org\/abs\/ 1907.00421."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.02.010"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.049"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538917.1538920"},{"key":"e_1_2_1_13_1","volume-title":"CAMP: Cost-Aware Multiparty Session Protocols. PACMPL SPLASH\/OOPSLA ( 2020 ), 30 pages. To appear.","author":"Castro-Perez David","year":"2020","unstructured":"David Castro-Perez and Nobuko Yoshida . 2020 a. CAMP: Cost-Aware Multiparty Session Protocols. PACMPL SPLASH\/OOPSLA ( 2020 ), 30 pages. To appear. David Castro-Perez and Nobuko Yoshida. 2020a. CAMP: Cost-Aware Multiparty Session Protocols. PACMPL SPLASH\/OOPSLA ( 2020 ), 30 pages. To appear."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377555.3377889"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(2:12)2017"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643138"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_19"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2015.560"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_10"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794275860"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.13052\/rp-9788793519817"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.002"},{"key":"e_1_2_1_27_1","volume-title":"Precise Subtyping for Asynchronous Multiparty Sessions (Extended Version). Available at: https:\/\/arxiv.org\/abs\/","author":"Ghilezan Silvia","year":"2010","unstructured":"Silvia Ghilezan , Jovanka Pantovi\u0107 , Ivan Proki\u0107 , Alceste Scalas , and Nobuko Yoshida . 2020. Precise Subtyping for Asynchronous Multiparty Sessions (Extended Version). Available at: https:\/\/arxiv.org\/abs\/ 2010 .13925. Silvia Ghilezan, Jovanka Pantovi\u0107, Ivan Proki\u0107, Alceste Scalas, and Nobuko Yoshida. 2020. Precise Subtyping for Asynchronous Multiparty Sessions (Extended Version). Available at: https:\/\/arxiv.org\/abs\/ 2010.13925."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90136-6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.12"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.13052\/rp-9788793519817"},{"key":"e_1_2_1_34_1","volume-title":"Shin","author":"Huang Hai","year":"2002","unstructured":"Hai Huang , Padmanabhan Pillai , and Kang G . Shin . 2002 . Improving Wait-Free Algorithms for Interprocess Communication in Embedded Real-Time Systems. In USENIX Annual Technical Conference, General Track . https:\/\/www.usenix.org\/legacy\/ event\/usenix02\/full_papers\/huang\/huang.pdf Hai Huang, Padmanabhan Pillai, and Kang G. Shin. 2002. Improving Wait-Free Algorithms for Interprocess Communication in Embedded Real-Time Systems. In USENIX Annual Technical Conference, General Track. https:\/\/www.usenix.org\/legacy\/ event\/usenix02\/full_papers\/huang\/huang.pdf"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994596"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.02.002"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_11"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_2_1_43_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press . Benjamin C. Pierce. 2002. Types and programming languages. MIT Press."},{"key":"e_1_2_1_44_1","volume-title":"Pierce and Davide Sangiorgi","author":"Benjamin","year":"1996","unstructured":"Benjamin C. Pierce and Davide Sangiorgi . 1996 . Typing and Subtyping for Mobile Processes. Mathematical Structures in Computer Science 6, 5 ( 1996 ), 409-453. Benjamin C. Pierce and Davide Sangiorgi. 1996. Typing and Subtyping for Mobile Processes. Mathematical Structures in Computer Science 6, 5 ( 1996 ), 409-453."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04167-9_12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434297","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434297","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434297"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434297"],"URL":"https:\/\/doi.org\/10.1145\/3434297","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}