Possible worlds and resources: The semantics of \(\mathbf{BI}\)

DOI10.1016/j.tcs.2003.11.020zbMath1055.03021OpenAlexW2013474929WikidataQ56445145 ScholiaQ56445145MaRDI QIDQ1826634

Peter W. O'Hearn, Hongseok Yang, David J. Pym

Publication date: 6 August 2004

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2003.11.020

zbMATH Keywords

possible-worlds semanticslogic of bunched implicationslogic of resources

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Categorical logic, topoi (03G30) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Bunched sequential information, Symbolic execution proofs for higher order store programs, From IF to BI. A tale of dependence and separation, Linear and affine logics with temporal, spatial and epistemic operators, A logic of separating modalities, Bringing Order to the Separation Logic Jungle, A Unified Display Proof Theory for Bunched Logic, Undecidability of Propositional Separation Logic and Its Neighbours, Separation logic and logics with team semantics, THE LOGIC OF RESOURCES AND CAPABILITIES, Coalgebraic completeness-via-canonicity for distributive substructural logics, Blaming the client: on data refinement in the presence of pointers, Temporal BI: proof system, semantics and translations, Separation logics and modalities: a survey, Non-normal modalities in variants of linear logic, Bunched logics displayed, Lewis meets Brouwer: constructive strict implication, Semantical analysis of the logic of bunched implications, An algebraic glimpse at bunched implications and separation logic, Local local reasoning: a BI-hyperdoctrine for full ground store, A calculus and logic of bunched resources and processes, Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials, Bunched polymorphism, Focused proof-search in the logic of bunched implications, A program logic for resources, Footprints in Local Reasoning, The virtues of idleness: a decidable fragment of resource agent logic, A step-indexed Kripke model of hidden state, Algebra and logic for access control, Algebraic separation logic, A coordination approach to mobile components, Unnamed Item, Graphical models of separation logic, Intuitionistic Layered Graph Logic, A Substructural Epistemic Resource Logic, Algebra and logic for resource-based systems modelling, On Model Checking Boolean BI, Towards a theory of resource: an approach based on soft exponentials, Separation Logic Tutorial, Modal algebra and Petri nets, Local Reasoning about Data Update, Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic, On the relation between concurrent separation logic and concurrent Kleene algebra

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Region-based memory management
• Sheaves in geometry and logic: a first introduction to topos theory
• Completeness results for linear logic on Petri nets
• The semantics and proof theory of the logic of bunched implications
• Reports of the Midwest category seminar. IV
• Uniform proofs as a foundation for logic programming
• The undecidability of entailment and relevant implication
• Contributions to the Theory of Logic Programming
• The Semantics of Predicate Logic as a Programming Language
• A relevant analysis of natural deduction
• The Logic of Bunched Implications
• Constructive Sheaf Semantics
• The finite model property for various fragments of linear logic
• On bunched typing
• TQL: a query language for semistructured data based on the ambient logic
• The Functional Approach to Programming
• Anytime, anywhere
• BI as an assertion language for mutable data structures
• Deductive systems and categories