{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:46:50Z","timestamp":1767926810470,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908965","type":"print"},{"value":"9783031908972","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We revisit the foundational notion of \u201cresources\u201d used by separation logics from a categorical\u00a0and algebraic viewpoint. In particular, we show that the <jats:italic>cameras<\/jats:italic> used by concurrent, higher-order, impredicative separation logics like Iris as a generalization of partial commutative monoids can be simplified and clarified and we introduce a category of cameras in\u00a0which many vital cameras exhibit simple universal properties. We do this by observing that an important structure on cameras (the <jats:italic>core<\/jats:italic> operator) can be uniquely constrained and replaced by\u00a0the property governing the idempotent elements of the camera. We verify that all cameras used\u00a0in practice in Iris satisfy this property and use this insight to simplify the existing\u00a0Iris formalization.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_3","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:05Z","timestamp":1746001025000},"page":"45-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Idempotent Resources in Separation Logic"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias Adam","family":"M\u00f8ller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 23(5), 657\u2013683 (2001)","DOI":"10.1145\/504709.504712"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: Bi-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29(5), 24\u2013es (Aug 2007), https:\/\/doi.org\/10.1145\/1275497.1275499","DOI":"10.1145\/1275497.1275499"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8(4) (2012)","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Bizjak, A., Birkedal, L.: On models of higher-order separation logic. Electronic Notes in Theoretical Computer Science 336, 57\u201378 (04 2018), https:\/\/doi.org\/10.1016\/j.entcs.2018.03.016","DOI":"10.1016\/j.entcs.2018.03.016"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 259\u2013270. ACM (2005), https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic.In: 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings. pp. 366\u2013378. IEEE Computer Society (2007), https:\/\/doi.org\/10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Dardinier, T., Parthasarathy, G., M\u00fcller, P.: Verification-preserving inlining in automatic separation logic verifiers. Proceedings of the ACM on Programming Languages 7(OOPSLA1), 789\u2013818 (Apr 2023)","DOI":"10.1145\/3586054"},{"key":"3_CR8","unstructured":"Day, B.: On closed categories of functors. In: MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc, E., Phreilambud, Pultr, A., Street, R., Tierney, M., Swierczkowski, S. (eds.) Reports of the Midwest Category Seminar IV. pp. 1\u201338. Springer Berlin Heidelberg, Berlin, Heidelberg (1970)"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy - January 23 - 25, 2013. pp. 287\u2013300. ACM (2013), https:\/\/doi.org\/10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5904, pp. 161\u2013177. Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Ahmed, A., Birkedal, L.: Logical step-indexed logical relations. Logical Methods in Computer Science Volume 7, Issue 2 (06 2011)","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Gratzer, D., M\u00f8ller, M.A., Birkedal, L.: Coq formalization accompanying \u201cIdempotent Resources in Separation Logic\u201d (2025), https:\/\/doi.org\/10.5281\/zenodo.14765017","DOI":"10.5281\/zenodo.14765017"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Syntax and Semantics of Dependent Types. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, pp. 79\u2013130. Cambridge University Press (1997), https:\/\/www.tcs.ifi.lmu.de\/mitarbeiter\/martin-hofmann\/pdfs\/syntaxandsemanticsof-dependenttypes.pdf","DOI":"10.1017\/CBO9780511526619.004"},{"key":"3_CR14","unstructured":"Hofmann, M., Streicher, T.: Lifting Grothendieck universes (1997), https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/NOTES\/lift.pdf, unpublished note"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: Bi as an assertion language for mutable data structures.In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL01, vol.\u00a07, p. 14\u201326. ACM (01 2001), https:\/\/doi.org\/10.1145\/360204.375719","DOI":"10.1145\/360204.375719"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Seidl, H. (ed.) Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7211, pp. 377\u2013396. Springer (2012), URL https:\/\/doi.org\/10.1007\/978-3-642-28869-2_19","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Birkedal, L., Dreyer, D.: Higher-order ghost state. SIGPLAN Not. 51(9), 256\u2013269 (09 2016)","DOI":"10.1145\/3022670.2951943"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. SIGPLAN Not. 50(1), 637\u2013650 (01 2015)","DOI":"10.1145\/2775051.2676980"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.H., Dreyer, D., Birkedal, L.: The Essence of Higher-Order Concurrent Separation Logic, p. 696\u2013723. Springer Berlin Heidelberg (2017), https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"3_CR21","unstructured":"Mac\u00a0Lane, S., Moerdijk, I.: Sheaves in geometry and logic : a first introduction to topos theory. Universitext, Springer (1992)"},{"key":"3_CR22","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures, p. 1\u201319. Springer Berlin Heidelberg (2001), https:\/\/doi.org\/10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5(2), 215\u2013244 (06 1999), https:\/\/doi.org\/10.2307\/421090","DOI":"10.2307\/421090"},{"key":"3_CR24","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science (2002)"},{"key":"3_CR25","unstructured":"Rosolini, G.: Continuity and effectiveness in topoi. Ph.D. thesis, University of Oxford (1986)"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Spies, S., G\u00e4her, L., Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D., Birkedal, L.: Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic, p. 80\u201395. Association for Computing Machinery, New York, NY, USA (2021), https:\/\/doi.org\/10.1145\/3453483.3454031","DOI":"10.1145\/3453483.3454031"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90897-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:16Z","timestamp":1746001036000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_3"}},"subtitle":["The Heart of core in Iris"],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}