{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:08Z","timestamp":1772164028629,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535844","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"453-464","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Parametric completeness for separation theories"],"prefix":"10.1145","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[{"name":"University College London, London, United Kingdom"}]},{"given":"Jules","family":"Villard","sequence":"additional","affiliation":[{"name":"University College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/381193"},{"key":"e_1_3_2_2_2_1","volume-title":"ten Cate. Pure extensions, proof rules, and hybrid axiomatics. Studia Logica, 84(2)","author":"Blackburn P.","year":"2006","unstructured":"P. Blackburn and B. ten Cate. Pure extensions, proof rules, and hybrid axiomatics. Studia Logica, 84(2) , 2006 . P. Blackburn and B. ten Cate. Pure extensions, proof rules, and hybrid axiomatics. Studia Logica, 84(2), 2006."},{"key":"e_1_3_2_2_3_1","series-title":"Wiley series in probability and mathematical statistics","volume-title":"Empirical model-building and response surfaces","author":"Box G. E. P.","year":"1987","unstructured":"G. E. P. Box and N. R. Draper . Empirical model-building and response surfaces . Wiley series in probability and mathematical statistics . John Wiley & Sons, Inc. , 1987 . G. E. P. Box and N. R. Draper. Empirical model-building and response surfaces. Wiley series in probability and mathematical statistics. John Wiley & Sons, Inc., 1987."},{"key":"e_1_3_2_2_4_1","volume-title":"Classical BI: Its semantics and proof theory. Logical Methods in Computer Science, 6(3)","author":"Brotherston J.","year":"2010","unstructured":"J. Brotherston and C. Calcagno . Classical BI: Its semantics and proof theory. Logical Methods in Computer Science, 6(3) , 2010 . J. Brotherston and C. Calcagno. Classical BI: Its semantics and proof theory. Logical Methods in Computer Science, 6(3), 2010."},{"key":"e_1_3_2_2_5_1","author":"Brotherston J.","unstructured":"J. Brotherston and M. Kanovich . Undecidability of propositional separation logic and its neighbours. To appear in phJournal of the ACM. J. Brotherston and M. Kanovich. Undecidability of propositional separation logic and its neighbours. To appear in phJournal of the ACM.","journal-title":"Undecidability of propositional separation logic and its neighbours. To appear in phJournal of the ACM."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190236"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529402"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048096"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_3_2_2_13_1","volume-title":"Constraint-based program reasoning with heaps and separation","author":"Duck G. J.","year":"2013","unstructured":"G. J. Duck , J. Jaffar , and N. C. H. Koh . Constraint-based program reasoning with heaps and separation . 2013 . To appear in CP- 19. G. J. Duck, J. Jaffar, and N. C. H. Koh. Constraint-based program reasoning with heaps and separation. 2013. To appear in CP-19."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_33"},{"key":"e_1_3_2_2_15_1","unstructured":"K. G\u00f6del. On formally undecidable propositions of Principia Mathematica and related systems. 1962. English translation by B. Meltzer.  K. G\u00f6del. On formally undecidable propositions of Principia Mathematica and related systems. 1962. English translation by B. Meltzer."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_3_2_2_17_1","volume-title":"A labelled sequent calculus for Boolean BI: Proof theory and proof search. To appear in TABLEAUX-22","author":"Hou Z.","year":"2013","unstructured":"Z. Hou , A. Tiu , and R. Gor\u00e9 . A labelled sequent calculus for Boolean BI: Proof theory and proof search. To appear in TABLEAUX-22 , 2013 . Z. Hou, A. Tiu, and R. Gor\u00e9. A labelled sequent calculus for Boolean BI: Proof theory and proof search. To appear in TABLEAUX-22, 2013."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_2_19_1","volume-title":"The formal strong completeness of Boolean BI. Submitted","author":"Larchey-Wendling D.","year":"2012","unstructured":"D. Larchey-Wendling . The formal strong completeness of Boolean BI. Submitted , 2012 . D. Larchey-Wendling. The formal strong completeness of Boolean BI. Submitted, 2012."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007567"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.18"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429095"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0091-7"},{"key":"e_1_3_2_2_24_1","volume-title":"LICS-17","author":"Reynolds J. C.","year":"2002","unstructured":"J. C. Reynolds . Separation logic : A logic for shared mutable data structures . In LICS-17 . IEEE Computer Society , 2002 . J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS-17. IEEE Computer Society, 2002."},{"key":"e_1_3_2_2_25_1","unstructured":"J. C. Reynolds. A short course on separation logic. http:\/\/www.cs.cmu.edu\/afs\/cs.cmu.edu\/project\/fox-19\/member\/jcr\/wwwaac2003\/aac.html 2003.  J. C. Reynolds. A short course on separation logic. http:\/\/www.cs.cmu.edu\/afs\/cs.cmu.edu\/project\/fox-19\/member\/jcr\/wwwaac2003\/aac.html 2003."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535844","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:39:24Z","timestamp":1750221564000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":26,"alternative-id":["10.1145\/2535838.2535844","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535844","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535844","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}