{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:23:36Z","timestamp":1770283416708,"version":"3.49.0"},"reference-count":38,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,9,1]],"date-time":"2011-09-01T00:00:00Z","timestamp":1314835200000},"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 develop local reasoning techniques for message passing concurrent programs based on ideas from separation logics and resource usage analysis. We extend processes with permission- resources and define a reduction semantics for this extended language. This provides a foundation for interpreting separation formulas for message-passing concurrency. We also define a sound proof system permitting us to infer satisfaction compositionally using local, separation-based reasoning.<\/jats:p>","DOI":"10.2168\/lmcs-7(3:7)2011","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T13:45:24Z","timestamp":1415972724000},"source":"Crossref","is-referenced-by-count":5,"title":["Permission-Based Separation Logic for Message-Passing Concurrency"],"prefix":"10.46298","volume":"Volume 7, Issue 3","author":[{"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[]},{"given":"Julian","family":"Rathke","sequence":"additional","affiliation":[]},{"given":"Vladimiro","family":"Sassone","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2011,9,1]]},"reference":[{"key":"10.2168\/LMCS-7(3:7)2011_AmDam96","doi-asserted-by":"crossref","unstructured":"R. Amadio and M. Dam. Toward a modal theory of types for thepi-calculus. InFTRTFT, volume 1135 ofLNCS, 1996.","DOI":"10.1007\/3-540-61648-9_50"},{"key":"10.2168\/LMCS-7(3:7)2011_AnStWi94","doi-asserted-by":"crossref","unstructured":"H. Andersen, C. Stirling, and G. Winskel. A compositional proof system for the modal\u00ce\u00bc-calculus. InLICS, volume 4-7, pages 144-153, 1994.","DOI":"10.1109\/LICS.1994.316076"},{"key":"10.2168\/LMCS-7(3:7)2011_Armstrong07","unstructured":"J. Armstrong.Programming Erlang. Pragmatic Bookshelf, 2007."},{"key":"10.2168\/LMCS-7(3:7)2011_BergerHondaYoshida08","doi-asserted-by":"crossref","unstructured":"M. Berger, K. Honda, and N. Yoshida. Completeness and full abstraction in modal logics for typed mobile processes. InICALP, volume 5126 ofLNCS, pages 99-111, 2008.","DOI":"10.1007\/978-3-540-70583-3_9"},{"key":"10.2168\/LMCS-7(3:7)2011_permission","doi-asserted-by":"crossref","unstructured":"R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. InPOPL, pages 259-270, 2005.","DOI":"10.1145\/1047659.1040327"},{"key":"10.2168\/LMCS-7(3:7)2011_Boyland03","doi-asserted-by":"crossref","unstructured":"J. Boyland. Checking interference with fractional permissions. InSAS, volume 2694 ofLNCS, pages 55-72, 2003.","DOI":"10.1007\/3-540-44898-5_4"},{"issue":"1-3","key":"10.2168\/LMCS-7(3:7)2011_Brookes07","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S. Brookes","year":"2007","journal-title":"TCS"},{"key":"10.2168\/LMCS-7(3:7)2011_Caires01","doi-asserted-by":"crossref","unstructured":"L. Caires and L. Cardelli. A spatial logic for concurrency (i).I AND C, pages 1-37, 2001.","DOI":"10.1007\/3-540-45500-0_1"},{"issue":"3","key":"10.2168\/LMCS-7(3:7)2011_Caires04","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1016\/j.tcs.2003.10.041","volume":"322","author":"L. Caires and L. Cardelli","year":"2004","journal-title":"TCS"},{"key":"10.2168\/LMCS-7(3:7)2011_Calcagno07localaction","doi-asserted-by":"crossref","unstructured":"C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. InLICS, pages 366-378, 2007.","DOI":"10.1109\/LICS.2007.30"},{"key":"10.2168\/LMCS-7(3:7)2011_Calcagno07modularsafety","doi-asserted-by":"crossref","unstructured":"C. Calcagno, M. Parkinson, and V. Vafeiadis. Modular safety checking for fine-grained concurrency. InSAS, volume 4634 ofLNCS, pages 233-238, 2007.","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"10.2168\/LMCS-7(3:7)2011_Dam94","doi-asserted-by":"crossref","unstructured":"M. Dam. Model checking mobile processes. InCONCUR, volume 715 ofLNCS, pages 22-36, 1993.","DOI":"10.1007\/3-540-57208-2_3"},{"key":"10.2168\/LMCS-7(3:7)2011_Dam02","doi-asserted-by":"publisher","DOI":"10.1007\/0-306-48088-3_4"},{"key":"10.2168\/LMCS-7(3:7)2011_dodds09:denyguarantee","doi-asserted-by":"crossref","unstructured":"Mike Dodds, Xinyu Feng, Matthew Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. InESOP 2009, volume 5502 ofLNCS, pages 363-377, 2009.","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"10.2168\/LMCS-7(3:7)2011_Feng","doi-asserted-by":"crossref","unstructured":"X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. InESOP, pages 173-188, 2007.","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"10.2168\/LMCS-7(3:7)2011_Galletly97","unstructured":"J. Galletly.Occam-2 (2nd ed.): including occam.2.1. UCL Press, 1997."},{"key":"10.2168\/LMCS-7(3:7)2011_Girard:1989","unstructured":"Jean-Yves Girard, Paul Taylor, and Yves Lafont.Proofs and types. Cambridge University Press, New York, NY, USA, 1989."},{"key":"10.2168\/LMCS-7(3:7)2011_Gotsman","doi-asserted-by":"crossref","unstructured":"A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local reasoning for storable locks and threads. InAPLAS, volume 4807 ofLNCS, pages 19-37, 2007.","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"10.2168\/LMCS-7(3:7)2011_HennessyLin96","doi-asserted-by":"crossref","unstructured":"M. Hennessy and H. Lin. Proof systems for message-passing process algebras. InFormal Aspects of Computing, pages 379-407, 1996.","DOI":"10.1007\/BF01213531"},{"key":"10.2168\/LMCS-7(3:7)2011_Hliu93","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF01178384","volume":"32","author":"M. Hennessy and H. Liu","year":"1995","journal-title":"Act. Inf."},{"issue":"8","key":"10.2168\/LMCS-7(3:7)2011_Hoare78","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C. A. R. Hoare","year":"1978","journal-title":"Comm. ACM"},{"key":"10.2168\/LMCS-7(3:7)2011_HoareOhearn","first-page":"3","volume":"212","author":"T. Hoare and P. O'Hearn","year":"2008","journal-title":"ENTCS"},{"key":"10.2168\/LMCS-7(3:7)2011_Knuth98","unstructured":"Donald E. Knuth.The art of computer programming, volume 3: (2nd ed.) sorting and searching. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1998."},{"issue":"5","key":"10.2168\/LMCS-7(3:7)2011_KobayashiPT:linearity","doi-asserted-by":"crossref","first-page":"914","DOI":"10.1145\/330249.330251","volume":"21","author":"Naoki Kobayashi, Benjamin C. Pierce, and","year":"1999","journal-title":"ACM ToPLaS"},{"key":"10.2168\/LMCS-7(3:7)2011_Lynch96","unstructured":"Nancy A. Lynch.Distributed Algorithms. Morgan Kaufmann, 1996."},{"key":"10.2168\/LMCS-7(3:7)2011_Milner89","unstructured":"R. Milner.Communication and concurrency. Prentice-Hall, 1989."},{"key":"10.2168\/LMCS-7(3:7)2011_Milner99","unstructured":"R. Milner.Communicating and mobile systems: thepi-calculus. Cambridge Univ., 1999."},{"key":"10.2168\/LMCS-7(3:7)2011_Ohearn04","doi-asserted-by":"crossref","unstructured":"P. W. O'Hearn. Resources, concurrency and local reasoning.TCS, pages 49-67, 2004.","DOI":"10.1007\/978-3-540-28644-8_4"},{"issue":"1","key":"10.2168\/LMCS-7(3:7)2011_ParkinsonBornat","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1145\/1190215.1190261","volume":"42","author":"M. Parkinson, R. Bornat, et. al","year":"2007","journal-title":"SIGPLAN Not."},{"key":"10.2168\/LMCS-7(3:7)2011_presburger29","unstructured":"Mojzesz Presburger. \u00dcber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. InComptes Rendus du I congr\u00c3\u00a8s de Math\u00c3\u00a9maticiens des Pays Slaves, pages 92-101, 1929."},{"key":"10.2168\/LMCS-7(3:7)2011_PymTofts","first-page":"495","volume":"18","author":"D. Pym and C. Tofts","year":"2006","journal-title":"FAC"},{"key":"10.2168\/LMCS-7(3:7)2011_Reppy99","doi-asserted-by":"crossref","unstructured":"J. H. Reppy.Concurrent programming in ML. Cambridge University Press, 1999.","DOI":"10.1017\/CBO9780511574962"},{"key":"10.2168\/LMCS-7(3:7)2011_Reynolds02","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Separation logic: A logic for shared mutable data structures. InLICS, pages 55-74, 2002.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"10.2168\/LMCS-7(3:7)2011_SangiorgiWalker01","unstructured":"D. Sangiorgi and D. Walker.PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2001."},{"key":"10.2168\/LMCS-7(3:7)2011_Stirling01","doi-asserted-by":"crossref","unstructured":"C. Stirling.Modal and temporal properties of processes. Springer-Verlag, 2001.","DOI":"10.1007\/978-1-4757-3550-5"},{"issue":"5","key":"10.2168\/LMCS-7(3:7)2011_TerauchiAiken08","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1387673.1387676","volume":"30","author":"T. Terauchi and A. Aiken","year":"2008","journal-title":"TOPLAS"},{"key":"10.2168\/LMCS-7(3:7)2011_Vafeiadis07amarriage","doi-asserted-by":"crossref","unstructured":"V. Vafeiadis and M. Parkinson. A marriage of rely\/guarantee and separation logic. InCONCUR, pages 256-271, 2007.","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"10.2168\/LMCS-7(3:7)2011_Villard09","doi-asserted-by":"crossref","unstructured":"J. Villard, \u00c9. Lozes, and C. Calcagno. Proving copyless message passing. InAPLAS'09, volume 5904 ofLNCS, pages 194-209, Seoul, Korea, 2009.","DOI":"10.1007\/978-3-642-10672-9_15"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/772\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/772\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T18:03:13Z","timestamp":1747159393000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/772"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,1]]},"references-count":38,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(3:7)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1106.5128","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1106.5128","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1145\/3371074","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9,1]]},"article-number":"772"}}