{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:50:12Z","timestamp":1775868612626,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2023,4,30]],"date-time":"2023-04-30T00:00:00Z","timestamp":1682812800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"EU Horizon 2020","award":["830929 EUH2020"],"award-info":[{"award-number":["830929 EUH2020"]}]},{"name":"EU COST","award":["SP4670, CA15123 SP4670 and IC1201 SP4670"],"award-info":[{"award-number":["SP4670, CA15123 SP4670 and IC1201 SP4670"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","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, EP\/X015955\/1"],"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, EP\/X015955\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"NCSS\/EPSRC VeTSS"},{"name":"MPNTR MPNTR and SFRS SFRS","award":["6526707 SFRS and 6458932 SFRS"],"award-info":[{"award-number":["6526707 SFRS and 6458932 SFRS"]}]},{"name":"Danmark Industriens Fond DIF","award":["2020-0489 DIF"],"award-info":[{"award-number":["2020-0489 DIF"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,4,30]]},"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            \u2264\n            <jats:italic>T<\/jats:italic>\n            \u2032 holds, it is safe to replace an implementation of\u00a0\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. 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). 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. Our session decomposition technique expresses the subtyping relation as a composition of refinement relations between single input\/output trees and provides a simple reasoning principle for asynchronous message optimisations.\n          <\/jats:p>","DOI":"10.1145\/3568422","type":"journal-article","created":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T11:52:38Z","timestamp":1666266758000},"page":"1-73","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Precise Subtyping for Asynchronous Multiparty Sessions"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2253-8285","authenticated-orcid":false,"given":"Silvia","family":"Ghilezan","sequence":"first","affiliation":[{"name":"Univerzitet u Novom Sadu, Novi Sad, Serbia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3974-5064","authenticated-orcid":false,"given":"Jovanka","family":"Pantovi\u0107","sequence":"additional","affiliation":[{"name":"Univerzitet u Novom Sadu, Novi Sad, Serbia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5420-1527","authenticated-orcid":false,"given":"Ivan","family":"Proki\u0107","sequence":"additional","affiliation":[{"name":"Univerzitet u Novom Sadu, Novi Sad, Serbia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1153-6164","authenticated-orcid":false,"given":"Alceste","family":"Scalas","sequence":"additional","affiliation":[{"name":"Technical University of Denmark, Kongens Lyngby, DK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3925-8557","authenticated-orcid":false,"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,11,6]]},"reference":[{"key":"e_1_3_4_2_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_3_4_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_3_4_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_3_4_5_1","volume-title":"Completely Subtyping Iso-recursive Types","author":"Blackburn Jeremy","year":"2012","unstructured":"Jeremy Blackburn, Ivory Hernandez, Jay Ligatti, and Michael Nachtigal. 2012. Completely Subtyping Iso-recursive Types. Technical Report CSE-071012. University of South Florida."},{"key":"e_1_3_4_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_3_4_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2019.38"},{"key":"e_1_3_4_8_1","unstructured":"Mario Bravetti Marco Carbone Julien Lange Nobuko Yoshida and Gianluigi Zavattaro. 2019b. A Sound Algorithm for Asynchronous Session Subtyping (Extended Version). Retrieved from http:\/\/arxiv.org\/abs\/1907.00421."},{"key":"e_1_3_4_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.02.010"},{"key":"e_1_3_4_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"e_1_3_4_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_3"},{"key":"e_1_3_4_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538917.1538920"},{"key":"e_1_3_4_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.049"},{"key":"e_1_3_4_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428223"},{"key":"e_1_3_4_15_1","doi-asserted-by":"publisher","unstructured":"David Castro-Perez and Nobuko Yoshida. 2020. Compiling first-order functions to session-typed parallel code. In 29th International Conference on Compiler Construction.143\u2013154. DOI:10.1145\/3377555.3377889","DOI":"10.1145\/3377555.3377889"},{"key":"e_1_3_4_16_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(2:12)2017"},{"key":"e_1_3_4_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643138"},{"key":"e_1_3_4_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508404"},{"key":"e_1_3_4_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_19"},{"key":"e_1_3_4_20_1","doi-asserted-by":"publisher","unstructured":"Romain Demangeon and Nobuko Yoshida. 2015. On the expressiveness of multiparty sessions. 35th (IARCS) Annual Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS\u201915 December 16-18 2015 Bangalore India) Prahladh Harsha and G. Ramalingam (Eds.). Vol. 45 560\u2013574. 10.4230\/LIPIcs.FSTTCS.2015.560","DOI":"10.4230\/LIPIcs.FSTTCS.2015.560"},{"key":"e_1_3_4_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_10"},{"key":"e_1_3_4_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_3_4_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794275860"},{"key":"e_1_3_4_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_14"},{"key":"e_1_3_4_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_3_4_26_1","doi-asserted-by":"publisher","DOI":"10.13052\/rp-9788793519817"},{"key":"e_1_3_4_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_4_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.002"},{"key":"e_1_3_4_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434297"},{"key":"e_1_3_4_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90136-6"},{"key":"e_1_3_4_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_4_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_4_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_3_4_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.12"},{"key":"e_1_3_4_35_1","doi-asserted-by":"publisher","DOI":"10.13052\/rp-9788793519817"},{"key":"e_1_3_4_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"e_1_3_4_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_6"},{"key":"e_1_3_4_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2994596"},{"key":"e_1_3_4_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_3_4_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.02.002"},{"key":"e_1_3_4_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_3_4_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_11"},{"key":"e_1_3_4_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_3_4_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_4_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_3_4_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_3_4_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_3_4_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"e_1_3_4_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470531"},{"key":"e_1_3_4_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04167-9_12"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3568422","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3568422","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:33Z","timestamp":1750182693000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3568422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,30]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,4,30]]}},"alternative-id":["10.1145\/3568422"],"URL":"https:\/\/doi.org\/10.1145\/3568422","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,30]]},"assertion":[{"value":"2022-06-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-06","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}