{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:58Z","timestamp":1780994698538,"version":"3.54.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,6,10]],"date-time":"2022-06-10T00:00:00Z","timestamp":1654819200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Message passing is a useful abstraction for implementing concurrent programs.\nFor real-world systems, however, it is often combined with other programming\nand concurrency paradigms, such as higher-order functions, mutable state,\nshared-memory concurrency, and locks. We present Actris: a logic for proving\nfunctional correctness of programs that use a combination of the aforementioned\nfeatures. Actris combines the power of modern concurrent separation logics with\na first-class protocol mechanism -- based on session types -- for reasoning\nabout message passing in the presence of other concurrency paradigms. We show\nthat Actris provides a suitable level of abstraction by proving functional\ncorrectness of a variety of examples, including a channel-based merge sort, a\nchannel-based load-balancing mapper, and a variant of the map-reduce model,\nusing concise specifications. While Actris was already presented in a\nconference paper (POPL'20), this paper expands the prior presentation\nsignificantly. Moreover, it extends Actris to Actris 2.0 with a notion of\nsubprotocols -- based on session-type subtyping -- that permits additional\nflexibility when composing channel endpoints, and that takes full advantage of\nthe asynchronous semantics of message passing in Actris. Soundness of Actris\n2.0 is proven using a model of its protocol mechanism in the Iris framework. We\nhave mechanised the theory of Actris, together with custom tactics, as well as\nall examples in the paper, in the Coq proof assistant.<\/jats:p>","DOI":"10.46298\/lmcs-18(2:16)2022","type":"journal-article","created":{"date-parts":[[2022,6,13]],"date-time":"2022-06-13T14:12:01Z","timestamp":1655129521000},"source":"Crossref","is-referenced-by-count":12,"title":["Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic"],"prefix":"10.46298","volume":"Volume 18, Issue 2","author":[{"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jesper","family":"Bengtson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2022,6,10]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/9689\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/9689\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:18:18Z","timestamp":1687292298000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,10]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(2:16)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2010.15030v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2010.15030v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2010.15030","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2010.15030","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,6,10]]},"article-number":"6869"}}