{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:23Z","timestamp":1753894403118,"version":"3.41.2"},"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 formal specifications of communication protocols, allowing\nprotocol implementations to be verified by typechecking. Up to now, session\ntype disciplines have assumed that the communication medium is reliable, with\nno loss of messages. However, unreliable broadcast communication is common in a\nwide class of distributed systems such as ad-hoc and wireless sensor networks.\nOften such systems have structured communication patterns that should be\namenable to analysis by means of session types, but the necessary theory has\nnot previously been developed. We introduce the Unreliable Broadcast Session\nCalculus, a process calculus with unreliable broadcast communication, and equip\nit with a session type system that we show is sound. We capture two common\noperations, broadcast and gather, inhabiting dual session types. Message loss\nmay lead to non-synchronised session endpoints. To further account for\nunreliability we provide with an autonomous recovery mechanism that does not\nrequire acknowledgements from session participants. Our type system ensures\nsoundness, safety, and progress between the synchronised endpoints within a\nsession. We demonstrate the expressiveness of our framework by implementing\nPaxos, the textbook protocol for reaching consensus in an unreliable,\nasynchronous network.<\/jats:p>","DOI":"10.46298\/lmcs-20(3:13)2024","type":"journal-article","created":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T13:00:15Z","timestamp":1722862815000},"source":"Crossref","is-referenced-by-count":0,"title":["A Session Type System for Asynchronous Unreliable Broadcast Communication"],"prefix":"10.46298","volume":"Volume 20, Issue 3","author":[{"given":"Dimitrios","family":"Kouzapas","sequence":"first","affiliation":[]},{"given":"Ramunas Forsberg","family":"Gutkovas","sequence":"additional","affiliation":[]},{"given":"A. Laura","family":"Voinea","sequence":"additional","affiliation":[]},{"given":"Simon J.","family":"Gay","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,8,5]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/14024\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/14024\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T13:00:16Z","timestamp":1722862816000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/5567"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,5]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(3:13)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"1902.01353v3","asserted-by":"subject"},{"id-type":"arxiv","id":"1902.01353v2","asserted-by":"subject"},{"id-type":"arxiv","id":"1902.01353v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1902.01353","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1902.01353","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,8,5]]},"article-number":"5567"}}