{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:23Z","timestamp":1762459223418,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2014,6,26]],"date-time":"2014-06-26T00:00:00Z","timestamp":1403740800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We define a pi-calculus variant with a costed semantics where channels are\ntreated as resources that must explicitly be allocated before they are used and\ncan be deallocated when no longer required. We use a substructural type system\ntracking permission transfer to construct coinductive proof techniques for\ncomparing behaviour and resource usage efficiency of concurrent processes. We\nestablish full abstraction results between our coinductive definitions and a\ncontextual behavioural preorder describing a notion of process efficiency\nw.r.t. its management of resources. We also justify these definitions and\nrespective proof techniques through numerous examples and a case study\ncomparing two concurrent implementations of an extensible buffer.<\/jats:p>","DOI":"10.2168\/lmcs-10(2:15)2014","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T09:40:42Z","timestamp":1415958042000},"source":"Crossref","is-referenced-by-count":1,"title":["Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency"],"prefix":"10.46298","volume":"Volume 10, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[]},{"given":"Edsko","family":"DeVries","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Hennessy","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2014,6,26]]},"reference":[{"key":"816:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/691\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/691\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:55Z","timestamp":1681242835000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,26]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-10(2:15)2014","relation":{"is-same-as":[{"id-type":"arxiv","id":"1405.6100","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1405.6100","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2014,6,26]]},"article-number":"691"}}