{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:38Z","timestamp":1753889798785,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,3,19]],"date-time":"2008-03-19T00:00:00Z","timestamp":1205884800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A compositional Petri net-based semantics is given to a simple language\nallowing pointer manipulation and parallelism. The model is then applied to\ngive a notion of validity to the judgements made by concurrent separation logic\nthat emphasizes the process-environment duality inherent in such rely-guarantee\nreasoning. Soundness of the rules of concurrent separation logic with respect\nto this definition of validity is shown. The independence information retained\nby the Petri net model is then exploited to characterize the independence of\nparallel processes enforced by the logic. This is shown to permit a refinement\noperation capable of changing the granularity of atomic actions.<\/jats:p>","DOI":"10.2168\/lmcs-4(1:6)2008","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:27:13Z","timestamp":1212499633000},"source":"Crossref","is-referenced-by-count":3,"title":["Independence and concurrent separation logic"],"prefix":"10.46298","volume":"Volume 4, Issue 1","author":[{"given":"Jonathan","family":"Hayman","sequence":"first","affiliation":[]},{"given":"Glynn","family":"Winskel","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,3,19]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1100\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1100\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:29Z","timestamp":1681243409000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1100"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3,19]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(1:6)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0802.0820","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0802.0820","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,3,19]]},"article-number":"1100"}}