{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T18:02:44Z","timestamp":1763748164295,"version":"3.41.0"},"reference-count":108,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T00:00:00Z","timestamp":1555891200000},"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":["ACM SIGLOG News"],"published-print":{"date-parts":[[2019,4,22]]},"abstract":"<jats:p>\n            The Logic of Bunched Implications (BI) was introduced by O'Hearn and Pym. The original presentation of BI emphasised its role as a system for formal logic (broadly in the tradition of relevant logic) that has some interesting properties, combining a clean proof theory, including a categorical interpretation, with a simple truth-functional semantics. BI quickly found significant applications in program verification and program analysis, chiefly through a specific theory of BI that is commonly known as 'Separation Logic'. We survey the state of work in bunched logics - which, by now, is a quite large family of systems, including modal and epistemic logics and logics for layered graphs - in such a way as to organize the ideas into a coherent (semantic) picture with a strong interpretation in terms of resources. One such picture can be seen as deriving from an interpretation of BI's semantics in terms of\n            <jats:italic>resources,<\/jats:italic>\n            and this view provides a basis for a systematic interpretation of the family of bunched logics, including modal, epistemic, layered graph, and process-theoretic variants, in terms of resources. We explain the basic ideas of resource semantics, including comparisons with Linear Logic and ideas from economics and physics. We include discussions of BI's \u03bb-calculus, of Separation Logic, and of an approach to distributed systems modelling based on resource semantics.\n          <\/jats:p>","DOI":"10.1145\/3326938.3326940","type":"journal-article","created":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T16:24:44Z","timestamp":1585931084000},"page":"5-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Resource semantics"],"prefix":"10.1145","volume":"6","author":[{"given":"David","family":"Pym","sequence":"first","affiliation":[{"name":"UCL and The Alan Turing Institute, London"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,4,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-008-9415-6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275217"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.11.035"},{"key":"e_1_2_1_4_1","volume-title":"Entailment: Logic of Relevance and Necessity","author":"Anderson R.","year":"1992","unstructured":"R. Anderson and N. Belnap . Entailment: Logic of Relevance and Necessity , Volume 1 . Princeton University Press , 1992 . R. Anderson and N. Belnap. Entailment: Logic of Relevance and Necessity, Volume 1. Princeton University Press, 1992."},{"key":"e_1_2_1_5_1","volume-title":"Entailment: Logic of Relevance and Necessity","author":"Anderson R.","year":"1975","unstructured":"R. Anderson and N. Belnap . Entailment: Logic of Relevance and Necessity , Volume 2 . Princeton University Press , 1975 . R. Anderson and N. Belnap. Entailment: Logic of Relevance and Necessity, Volume 2. Princeton University Press, 1975."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_1_7_1","volume-title":"Category Theory for Computing Science","author":"Barr M.","year":"1998","unstructured":"M. Barr and C. Wells . Category Theory for Computing Science . Prentice Hall , 1998 . Available at http:\/\/www.math.mcgill.ca\/triples\/Barr-Wells-ctcs.pdf. Accessed 10 March 2019. M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, 1998. Available at http:\/\/www.math.mcgill.ca\/triples\/Barr-Wells-ctcs.pdf. Accessed 10 March 2019."},{"key":"e_1_2_1_8_1","volume-title":"Logical Dynamics of Information and Interaction","author":"van Benthem J.","year":"2014","unstructured":"J. van Benthem . Logical Dynamics of Information and Interaction . Cambridge University Press , 2014 . J. van Benthem. Logical Dynamics of Information and Interaction. Cambridge University Press, 2014."},{"issue":"13","key":"e_1_2_1_9_1","first-page":"309","article-title":"Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde","volume":"18","author":"Beth E.","year":"1955","unstructured":"E. Beth . Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde , N.R. Vol 18 , no 13 , 1955 , 309 -- 342 . E. Beth. Semantic entailment and formal derivability. Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, N.R. Vol 18, no 13, 1955, 309--342.","journal-title":"N.R."},{"key":"e_1_2_1_11_1","volume-title":"Generalized Galois Logics: Relational Semantics of Non-classical Calculi","author":"Bimb\u00f3 K.","year":"2008","unstructured":"K. Bimb\u00f3 and J. M. Dunn . Generalized Galois Logics: Relational Semantics of Non-classical Calculi . CSLI Publications , 2008 . K. Bimb\u00f3 and J. M. Dunn. Generalized Galois Logics: Relational Semantics of Non-classical Calculi. CSLI Publications, 2008."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_17"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CASON.2011.6085951"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-012-9449-0"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of CSL-24","author":"Brotherston J.","year":"2015","unstructured":"J. Brotherston and J. Villard . Sub-Classical Boolean Bunched Logics and the Meaning of Par . Proceedings of CSL-24 , LIPlcs, Dagstuhl, 325--342 , 2015 . J. Brotherston and J. Villard. Sub-Classical Boolean Bunched Logics and the Meaning of Par. Proceedings of CSL-24, LIPlcs, Dagstuhl, 325--342, 2015."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4108\/eai.24-8-2015.2260765"},{"key":"e_1_2_1_18_1","volume-title":"Relational semantics for full linear logic. Journal of Applied logic 12(1):50--66","author":"Coumans D.","year":"2014","unstructured":"D. Coumans , M. Gehrke , and L. van Rooijen . Relational semantics for full linear logic. Journal of Applied logic 12(1):50--66 , 2014 . D. Coumans, M. Gehrke, and L. van Rooijen. Relational semantics for full linear logic. Journal of Applied logic 12(1):50--66, 2014."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_10"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.04.040"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_1_22_1","first-page":"597","article-title":"A spatial logic for querying graphs. In Proc ICALP '02","volume":"2380","author":"Cardelli L.","year":"2002","unstructured":"L. Cardelli , P. Gardner , G. Ghelli . A spatial logic for querying graphs. In Proc ICALP '02 , LNCS 2380 , 597 -- 610 , 2002 . L. Cardelli, P. Gardner, G. Ghelli. A spatial logic for querying graphs. In Proc ICALP '02, LNCS 2380, 597--610, 2002.","journal-title":"LNCS"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/52325.52336"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.02.008"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu002"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exv020"},{"key":"e_1_2_1_27_1","volume-title":"A Discipline of Mathematical Systems Modelling","author":"Collinson M.","year":"2012","unstructured":"M. Collinson , B. Monahan , and D. Pym . A Discipline of Mathematical Systems Modelling . College Publications , 2012 . M. Collinson, B. Monahan, and D. Pym. A Discipline of Mathematical Systems Modelling. College Publications, 2012."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509990077"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0155-2"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_62"},{"key":"e_1_2_1_31_1","volume-title":"Pearson","author":"Coulouris G.","year":"2011","unstructured":"G. Coulouris , J. Dollimore , T. Kindberg , and G, Blair. Distributed Systems : Concepts and Design . Pearson , 2011 . G. Coulouris, J. Dollimore, T. Kindberg, and G, Blair. Distributed Systems: Concepts and Design. Pearson, 2011."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2012.07.002"},{"key":"e_1_2_1_33_1","volume-title":"Journal of Logic and Computation","author":"Courtault J.-R.","year":"2015","unstructured":"J.-R. Courtault and D. Galmiche . A modal separation logic for resource dynamics . Journal of Logic and Computation , 2015 . J.-R. Courtault and D. Galmiche. A modal separation logic for resource dynamics. Journal of Logic and Computation, 2015."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795279943"},{"key":"e_1_2_1_35_1","volume-title":"D. van Dalen. Logic and Structure.","year":"2008","unstructured":"D. van Dalen. Logic and Structure. 4 th Edition. Universitext, Springer , 2008 . D. van Dalen. Logic and Structure. 4th Edition. Universitext, Springer, 2008.","edition":"4"},{"key":"e_1_2_1_36_1","volume-title":"November","author":"Dang H.-H.","year":"2018","unstructured":"H.-H. Dang , J.-H. Jourdan , J.-O. Kaiser , and D. Dreyer . RustBelt Relaxed. Submitted for publication , November 2018 . H.-H. Dang, J.-H. Jourdan, J.-O. Kaiser, and D. Dreyer. RustBelt Relaxed. Submitted for publication, November 2018."},{"key":"e_1_2_1_37_1","first-page":"1","article-title":"On closed categories of functors. In: S. Mac Lane, editor","volume":"137","author":"Day B.","year":"1971","unstructured":"B. Day . On closed categories of functors. In: S. Mac Lane, editor , Reports of the Midwest Category Theory Seminar. Lecture Notes in Mathematics 137 : 1 -- 38 , 1971 . B. Day. On closed categories of functors. In: S. Mac Lane, editor, Reports of the Midwest Category Theory Seminar. Lecture Notes in Mathematics 137:1--38, 1971.","journal-title":"Reports of the Midwest Category Theory Seminar. Lecture Notes in Mathematics"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0063099"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_32"},{"key":"e_1_2_1_41_1","first-page":"101","article-title":"A Stone-type duality theorem for Separation Logic via its underlying bunched logics Electronic Notes","volume":"336","author":"Docherty S.","year":"2018","unstructured":"S. Docherty and D. Pym . A Stone-type duality theorem for Separation Logic via its underlying bunched logics Electronic Notes in Theoretical Computer Science 336 ( 2018 ) 101 -- 118 . S. Docherty and D. Pym. A Stone-type duality theorem for Separation Logic via its underlying bunched logics Electronic Notes in Theoretical Computer Science 336 (2018) 101--118.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"e_1_2_1_42_1","first-page":"1","article-title":"A Stone-type duality theorem for Separation Logic via its underlying bunched logics Logical Methods","volume":"15","author":"Docherty S.","year":"2019","unstructured":"S. Docherty and D. Pym . A Stone-type duality theorem for Separation Logic via its underlying bunched logics Logical Methods in Computer Science 15 ( 1 ) ( March 14, 2019 ), 27: 1 -- 27 :51. https:\/\/lmcs.episciences.org\/5284\/pdf. S. Docherty and D. Pym. A Stone-type duality theorem for Separation Logic via its underlying bunched logics Logical Methods in Computer Science 15(1) (March 14, 2019), 27:1--27:51. https:\/\/lmcs.episciences.org\/5284\/pdf.","journal-title":"Computer Science"},{"issue":"4","key":"e_1_2_1_43_1","first-page":"1","volume":"14","author":"Docherty S.","year":"2018","unstructured":"S. Docherty and D. Pym . Intuitionistic Layered Graph Logic: Semantics and Proof Theory Logical Methods in Computer Science 14 ( 4 ) ( October 31, 2018 ), 1 -- 36 . https:\/\/lmcs.episciences.org\/4942\/pdf. S. Docherty and D. Pym. Intuitionistic Layered Graph Logic: Semantics and Proof Theory Logical Methods in Computer Science 14(4) (October 31, 2018), 1--36. https:\/\/lmcs.episciences.org\/4942\/pdf.","journal-title":"Intuitionistic Layered Graph Logic: Semantics and Proof Theory Logical Methods in Computer Science"},{"key":"e_1_2_1_44_1","volume-title":"Dal Lago U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS","author":"Docherty S.","year":"2018","unstructured":"S. Docherty and D. Pym . Modular Tableaux Calculi for Separation Theories In: Baier C ., Dal Lago U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2018 . LNCS 10803: 441--458. Springer . S. Docherty and D. Pym. Modular Tableaux Calculi for Separation Theories In: Baier C., Dal Lago U. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2018. LNCS 10803:441--458. Springer."},{"key":"e_1_2_1_45_1","volume-title":"OUP","author":"Dunn J. M.","year":"2001","unstructured":"J. M. Dunn and G. Hardegree . Algebraic Methods In Philosophical Logic . OUP , 2001 . J. M. Dunn and G. Hardegree. Algebraic Methods In Philosophical Logic. OUP, 2001."},{"key":"e_1_2_1_46_1","first-page":"147","article-title":"Topological Kripke models","volume":"15","author":"Esakia L.","year":"1974","unstructured":"L. Esakia . Topological Kripke models . Soviet Math. Dokl. 15 , 147 -- 115 , 1974 . L. Esakia. Topological Kripke models. Soviet Math. Dokl. 15, 147--15, 1974.","journal-title":"Soviet Math. Dokl."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093894722"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000444"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-017-0456-x"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54069-5_9"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn066"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004858"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn066"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"volume-title":"Gabbay D.M., Hhnle R., Posegga J. (eds) Handbook of Tableau Methods, 297--396","author":"Gor\u00e9 R.","key":"e_1_2_1_55_1","unstructured":"R. Gor\u00e9 . Tableau Methods for Modal and Temporal Logics In: D?Agostino M ., Gabbay D.M., Hhnle R., Posegga J. (eds) Handbook of Tableau Methods, 297--396 . Springer , Dordrecht . R. Gor\u00e9. Tableau Methods for Modal and Temporal Logics In: D?Agostino M., Gabbay D.M., Hhnle R., Posegga J. (eds) Handbook of Tableau Methods, 297--396. Springer, Dordrecht."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10107-009-0297-2"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.031"},{"key":"e_1_2_1_58_1","first-page":"178","article-title":"Alan Robinson and Andrei Voronkov, editors, Hand-book of Automated Reasoning","volume":"101","author":"H\u00e4hnle Reiner","year":"2001","unstructured":"Reiner H\u00e4hnle . Tableaux and Related Methods . In : Alan Robinson and Andrei Voronkov, editors, Hand-book of Automated Reasoning , Springer , 2001 , 101 -- 178 . Reiner H\u00e4hnle. Tableaux and Related Methods. In: Alan Robinson and Andrei Voronkov, editors, Hand-book of Automated Reasoning, Springer, 2001, 101--178.","journal-title":"Springer"},{"key":"e_1_2_1_59_1","volume-title":"The finite embeddability property for residuated groupoids Algebra Univers., 72(1):1--13","author":"Hanikov\u00e1 Z.","year":"2014","unstructured":"Z. Hanikov\u00e1 and R. Hor\u010d\u00edk . The finite embeddability property for residuated groupoids Algebra Univers., 72(1):1--13 , 2014 . Z. Hanikov\u00e1 and R. Hor\u010d\u00edk. The finite embeddability property for residuated groupoids Algebra Univers., 72(1):1--13, 2014."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601778"},{"volume-title":"https:\/\/fbinfer.com: accessed","year":"2019","key":"e_1_2_1_61_1","unstructured":"Facebook. Infer. https:\/\/fbinfer.com: accessed 10 March 2019 . https:\/\/code.fb.com\/developer-tools\/open-sourcing-facebook-infer-identify-bugs-before-you-ship\/: accessed 10 March 2019. Facebook. Infer. https:\/\/fbinfer.com: accessed 10 March 2019. https:\/\/code.fb.com\/developer-tools\/open-sourcing-facebook-infer-identify-bugs-before-you-ship\/: accessed 10 March 2019."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/646234.758793"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_64_1","volume-title":"To H. B. Curry: Essays on Combnatory Logic, Lambda-Calculus, and Formalism, 479--490","author":"Howard W.","year":"1980","unstructured":"W. Howard . The formulae-as-types notion of construction. In J. P. Seldin and J. R. HindIey, editors, To H. B. Curry: Essays on Combnatory Logic, Lambda-Calculus, and Formalism, 479--490 . Academic Press , 1980 . W. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. HindIey, editors, To H. B. Curry: Essays on Combnatory Logic, Lambda-Calculus, and Formalism, 479--490. Academic Press, 1980."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3627-4_3"},{"key":"e_1_2_1_67_1","volume-title":"CUP","author":"Johnstone Stone Spaces P. T.","year":"1982","unstructured":"P. T. Johnstone Stone Spaces . Cambridge Studies In Advanced Mathematics 3 , CUP , 1982 . P. T. Johnstone Stone Spaces. Cambridge Studies In Advanced Mathematics 3, CUP, 1982."},{"key":"e_1_2_1_68_1","volume-title":"https:\/\/julialang.org. Accessed","author":"Programming Language The Julia","year":"2019","unstructured":"The Julia Programming Language . https:\/\/julialang.org. Accessed 10 March 2019 . The Julia Programming Language. https:\/\/julialang.org. Accessed 10 March 2019."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_70_1","volume-title":"Iris from the ground up. Submitted","author":"Jung R.","year":"2018","unstructured":"R. Jung , R. Krebbers , J.-H. Jourdan , L. Birkedal , and D. Dreyer . Iris from the ground up. Submitted , 2018 . Manuscript: https:\/\/people.mpi-sws.org\/~dreyer\/papers\/iris-ground-up\/paper.pdf. Accessed 10 March 2019. R. Jung, R. Krebbers, J.-H. Jourdan, L. Birkedal, and D. Dreyer. Iris from the ground up. Submitted, 2018. Manuscript: https:\/\/people.mpi-sws.org\/~dreyer\/papers\/iris-ground-up\/paper.pdf. Accessed 10 March 2019."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1093\/comnet\/cnu016"},{"key":"e_1_2_1_72_1","volume-title":"New Orleans","author":"Korzybski A.","year":"1931","unstructured":"A. Korzybski . Non-Aristotelian System and its Necessity for Rigour in Mathematics and Physics. Presented to the American Association for the Advancement of Science , New Orleans , Louisiana , 28 December 1931 . Reprinted in Science and Sanity, 1933, 747--761. A. Korzybski. Non-Aristotelian System and its Necessity for Rigour in Mathematics and Physics. Presented to the American Association for the Advancement of Science, New Orleans, Louisiana, 28 December 1931. Reprinted in Science and Sanity, 1933, 747--761."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.96.138701"},{"key":"e_1_2_1_75_1","volume-title":"Brno","author":"Lafont Y.","year":"1993","unstructured":"Y. Lafont . Introduction to Linear Logic. Lecture notes from TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science , Brno , Czech Republic , 1993 . Y. Lafont. Introduction to Linear Logic. Lecture notes from TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science, Brno, Czech Republic, 1993."},{"key":"e_1_2_1_76_1","volume-title":"Studies of Language and its Mathematical Aspects, 166--178","author":"Lambek J.","year":"1961","unstructured":"J. Lambek . On the calculus of syntactic types. In Studies of Language and its Mathematical Aspects, 166--178 , 1961 . J. Lambek. On the calculus of syntactic types. In Studies of Language and its Mathematical Aspects, 166--178, 1961."},{"volume-title":"P","author":"Lambek J.","key":"e_1_2_1_77_1","unstructured":"J. Lambek . From categorical grammar to bilinear logic. In P . Schroeder-Heister and K. Do\u0161en, editors, Substructural Logics , 207--237 J. Lambek. From categorical grammar to bilinear logic. In P. Schroeder-Heister and K. Do\u0161en, editors, Substructural Logics, 207--237"},{"key":"e_1_2_1_78_1","volume-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek J.","year":"1986","unstructured":"J. Lambek and P. Scott . Introduction to Higher-Order Categorical Logic . Cambridge University Press , 1986 . J. Lambek and P. Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1986."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu031"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.5555\/20468"},{"key":"e_1_2_1_81_1","series-title":"Lecture Notes in Mathematics 611","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066201","volume-title":"First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories","author":"Makkei M.","year":"1977","unstructured":"M. Makkei and G. Reyes . First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories . Lecture Notes in Mathematics 611 , 1977 . M. Makkei and G. Reyes. First Order Categorical Logic: Model-Theoretical Methods in the Theory of Topoi and Related Categories. Lecture Notes in Mathematics 611, 1977."},{"key":"e_1_2_1_82_1","volume-title":"Rule-based multi-level modeling of cell biological systems BMC Sys. Bio., 5(166)","author":"Maus C.","year":"2011","unstructured":"C. Maus , S. Rybacki , and A. M. Uhrmacher . Rule-based multi-level modeling of cell biological systems BMC Sys. Bio., 5(166) , 2011 . C. Maus, S. Rybacki, and A. M. Uhrmacher. Rule-based multi-level modeling of cell biological systems BMC Sys. Bio., 5(166), 2011."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.5555\/1540607"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004495"},{"key":"e_1_2_1_86_1","first-page":"286","article-title":"A Primer on Separation Logic. Software Safety and Security;","volume":"33","author":"O'Hearn P.","year":"2012","unstructured":"P. O'Hearn . A Primer on Separation Logic. Software Safety and Security; Tools for Analysis and Verification. NATO Science for Peace and Security Series 33 : 286 -- 318 , 2012 . P. O'Hearn. A Primer on Separation Logic. Software Safety and Security; Tools for Analysis and Verification. NATO Science for Peace and Security Series 33:286--318, 2012.","journal-title":"Tools for Analysis and Verification. NATO Science for Peace and Security Series"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90263-2"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2010.03.014"},{"key":"e_1_2_1_92_1","volume-title":"Computer Science Department","author":"G. Plotkin A","year":"1981","unstructured":"G. Plotkin A structural approach to operational semantics, DAIMIFN-19 , Computer Science Department , Aarhus University , 1981 . G. Plotkin A structural approach to operational semantics, DAIMIFN-19, Computer Science Department, Aarhus University, 1981."},{"key":"e_1_2_1_93_1","first-page":"15","article-title":"The origins of structural operational semantics","volume":"3","author":"Plotkin G.","year":"2004","unstructured":"G. Plotkin . The origins of structural operational semantics . Journal of Logic and Algebraic Programming 60--61 , 2004 , 3 -- 15 . G. Plotkin. The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60--61, 2004, 3--15.","journal-title":"Journal of Logic and Algebraic Programming 60--61"},{"key":"e_1_2_1_94_1","volume-title":"Natural Deduction. Almqvist and Wiksell","author":"Prawitz D.","year":"1965","unstructured":"D. Prawitz . Natural Deduction. Almqvist and Wiksell , 1965 . D. Prawitz. Natural Deduction. Almqvist and Wiksell, 1965."},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_96_1","volume-title":"Why Separation Logic Works. Philosophy and Technology","author":"Pym D.","year":"2018","unstructured":"D. Pym , J. Spring , and P. O'Hearn . Why Separation Logic Works. Philosophy and Technology ( 2018 ). D. Pym, J. Spring, and P. O'Hearn. Why Separation Logic Works. Philosophy and Technology (2018)."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0018-z"},{"key":"e_1_2_1_98_1","unstructured":"S. Read. Relevant Logic. Blackwell 1988.  S. Read. Relevant Logic. Blackwell 1988."},{"key":"e_1_2_1_99_1","volume-title":"Proc LICS '02","author":"Reynolds J.","year":"2002","unstructured":"J. Reynolds . Separation Logic : a logic for shared mutable data structures . In Proc LICS '02 , IEEE Comp. Soc. Press, 55--74 2002 . J. Reynolds. Separation Logic: a logic for shared mutable data structures. In Proc LICS '02, IEEE Comp. Soc. Press, 55--74 2002."},{"key":"e_1_2_1_100_1","volume-title":"The weakest link. https:\/\/www.schneier.com\/blog\/archives\/2005\/02\/the_weakest_lin.html. Schneier on Security, https:\/\/www.schneier.com","author":"Schneier B.","year":"2005","unstructured":"B. Schneier . The weakest link. https:\/\/www.schneier.com\/blog\/archives\/2005\/02\/the_weakest_lin.html. Schneier on Security, https:\/\/www.schneier.com , 2005 . Accessed 10 March 2019. B. Schneier. The weakest link. https:\/\/www.schneier.com\/blog\/archives\/2005\/02\/the_weakest_lin.html. Schneier on Security, https:\/\/www.schneier.com, 2005. Accessed 10 March 2019."},{"key":"e_1_2_1_101_1","volume-title":"Substructural Logics","author":"Schroeder-Heister P.","year":"1993","unstructured":"P. Schroeder-Heister and K. Do\u0161en , editors , Substructural Logics . Oxford University Press , 1993 . P. Schroeder-Heister and K. Do\u0161en, editors, Substructural Logics. Oxford University Press, 1993."},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19830291005"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90093-3"},{"key":"e_1_2_1_104_1","unstructured":"R. Smullyan. First-order Logic. Dover 1995.  R. Smullyan. First-order Logic. Dover 1995."},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90012-0"},{"key":"e_1_2_1_106_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Properties of Processes","author":"Stirling C.","year":"2001","unstructured":"C. Stirling . Modal and Temporal Properties of Processes . Springer , 2001 . C. Stirling. Modal and Temporal Properties of Processes. Springer, 2001."},{"key":"e_1_2_1_107_1","volume-title":"The theory of representations of Boolean algebras. Trans. <b>AMS<\/b> 40: 37--111","author":"Stone M.","year":"1936","unstructured":"M. Stone . The theory of representations of Boolean algebras. Trans. <b>AMS<\/b> 40: 37--111 , 1936 . M. Stone. The theory of representations of Boolean algebras. Trans. <b>AMS<\/b> 40: 37--111, 1936."},{"key":"e_1_2_1_108_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511611193","volume-title":"Dependence Logic","author":"V\u00e4\u00e4n\u00e4nen J.","year":"2007","unstructured":"J. V\u00e4\u00e4n\u00e4nen . Dependence Logic . Cambridge University Press , 2007 . J. V\u00e4\u00e4n\u00e4nen. Dependence Logic. Cambridge University Press, 2007."},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2008.07.090"},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704850"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326938.3326940","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3326938.3326940","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:25:32Z","timestamp":1750206332000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326938.3326940"}},"subtitle":["logic as a modelling technology"],"short-title":[],"issued":{"date-parts":[[2019,4,22]]},"references-count":108,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4,22]]}},"alternative-id":["10.1145\/3326938.3326940"],"URL":"https:\/\/doi.org\/10.1145\/3326938.3326940","relation":{},"ISSN":["2372-3491"],"issn-type":[{"type":"electronic","value":"2372-3491"}],"subject":[],"published":{"date-parts":[[2019,4,22]]},"assertion":[{"value":"2019-04-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}