{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T02:38:00Z","timestamp":1774579080942,"version":"3.50.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Session types are widely used as abstractions of asynchronous message passing\nsystems. Refinement for such abstractions is crucial as it allows improvements\nof a given component without compromising its compatibility with the rest of\nthe system. In the context of session types, the most general notion of\nrefinement is asynchronous session subtyping, which allows message emissions to\nbe anticipated w.r.t. a bounded amount of message consumptions. In this paper\nwe investigate the possibility to anticipate emissions w.r.t. an unbounded\namount of consumptions: to this aim we propose to consider fair compliance over\nasynchronous session types and fair refinement as the relation that preserves\nit. This allows us to propose a novel variant of session subtyping that\nleverages the notion of controllability from service contract theory and that\nis a sound characterisation of fair refinement. In addition, we show that both\nfair refinement and our novel subtyping are undecidable. We also present a\nsound algorithm which deals with examples that feature potentially unbounded\nbuffering. Finally, we present an implementation of our algorithm and an\nempirical evaluation of it on synthetic benchmarks.<\/jats:p>","DOI":"10.46298\/lmcs-20(4:5)2024","type":"journal-article","created":{"date-parts":[[2024,10,7]],"date-time":"2024-10-07T19:45:08Z","timestamp":1728330308000},"source":"Crossref","is-referenced-by-count":1,"title":["Fair Asynchronous Session Subtyping"],"prefix":"10.46298","volume":"Volume 20, Issue 4","author":[{"given":"Mario","family":"Bravetti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Lange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianluigi","family":"Zavattaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2024,10,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/14411\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/14411\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,7]],"date-time":"2024-10-07T19:45:08Z","timestamp":1728330308000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/12368"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(4:5)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2101.08181v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2101.08181v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2101.08181","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2101.08181","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,7]]},"article-number":"12368"}}