Possible worlds and resources: The semantics of BI

DOI10.1016/J.TCS.2003.11.020MaRDI QIDQ1826634zbMATH OpenOpenAlexDBLPWikidataFDO

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

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

logic of bunched implicationslogic of resourcespossible-worlds semantics

Mathematics Subject Classification ID

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

Recommendations

• The semantics and proof theory of the logic of bunched implications
• The semantics of BI and resource tableaux
• scientific article; zbMATH DE number 1231702
• Classical BI: Its Semantics and Proof Theory
• scientific article; zbMATH DE number 1948162

Cites work

• A relevant analysis of natural deduction
• Anytime, anywhere: modal logics for mobile ambients
• BI as an assertion language for mutable data structures
• Completeness results for linear logic on Petri nets
• Constructive Sheaf Semantics
• Contributions to the Theory of Logic Programming
• Deductive systems and categories
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 3664336 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 41225 (Why is no real title available?)
• scientific article; zbMATH DE number 3483531 (Why is no real title available?)
• scientific article; zbMATH DE number 3496100 (Why is no real title available?)
• scientific article; zbMATH DE number 1342284 (Why is no real title available?)
• scientific article; zbMATH DE number 515728 (Why is no real title available?)
• scientific article; zbMATH DE number 1028818 (Why is no real title available?)
• scientific article; zbMATH DE number 1106703 (Why is no real title available?)
• scientific article; zbMATH DE number 1489627 (Why is no real title available?)
• scientific article; zbMATH DE number 1765675 (Why is no real title available?)
• scientific article; zbMATH DE number 2086655 (Why is no real title available?)
• scientific article; zbMATH DE number 1907195 (Why is no real title available?)
• scientific article; zbMATH DE number 786489 (Why is no real title available?)
• scientific article; zbMATH DE number 868086 (Why is no real title available?)
• scientific article; zbMATH DE number 932649 (Why is no real title available?)
• scientific article; zbMATH DE number 1406807 (Why is no real title available?)
• scientific article; zbMATH DE number 3241254 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Linear logic
• On bunched typing
• Region-based memory management
• Reports of the Midwest category seminar. IV
• Sheaves in geometry and logic: a first introduction to topos theory
• The finite model property for various fragments of linear logic
• The Functional Approach to Programming
• The Logic of Bunched Implications
• The semantics and proof theory of the logic of bunched implications
• The Semantics of Predicate Logic as a Programming Language
• The undecidability of entailment and relevant implication
• TQL: a query language for semistructured data based on the ambient logic
• Uniform proofs as a foundation for logic programming

Cited in

(58)

• Lewis meets Brouwer: constructive strict implication
• A coordination approach to mobile components
• Bunched logics displayed
• Separation logic and logics with team semantics
• Local local reasoning: a BI-hyperdoctrine for full ground store
• Focused proof-search in the logic of bunched implications
• Modal algebra and Petri nets
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Linear and affine logics with temporal, spatial and epistemic operators
• Inconsistency-tolerant bunched implications
• Coalgebraic completeness-via-canonicity for distributive substructural logics
• A program logic for resources
• The semantics and proof theory of the logic of bunched implications
• Bunched sequential information
• Intuitionistic layered graph logic
• Local reasoning about data update
• Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
• Symbolic execution proofs for higher order store programs
• A logic of separating modalities
• A unified display proof theory for bunched logic
• Undecidability of propositional separation logic and its neighbours
• The semantics of BI and resource tableaux
• Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials
• Bunched polymorphism
• A Games Model of Bunched Implications
• Algebra and logic for resource-based systems modelling
• On Model Checking Boolean BI
• Towards a theory of resource: an approach based on soft exponentials
• Temporal BI: proof system, semantics and translations
• scientific article; zbMATH DE number 1231702 (Why is no real title available?)
• The Logic of Bunched Implications
• scientific article; zbMATH DE number 1948162 (Why is no real title available?)
• scientific article; zbMATH DE number 1765675 (Why is no real title available?)
• scientific article; zbMATH DE number 6970800 (Why is no real title available?)
• THE LOGIC OF RESOURCES AND CAPABILITIES
• Separation logics and modalities: a survey
• Non-normal modalities in variants of linear logic
• Kripke Resource Models of a Dependently-typed, Bunched  -calculus
• A step-indexed Kripke model of hidden state
• Bringing Order to the Separation Logic Jungle
• The virtues of idleness: a decidable fragment of resource agent logic
• A substructural epistemic resource logic
• Footprints in Local Reasoning
• Algebraic separation logic
• Separation Logic Tutorial
• Blaming the client: on data refinement in the presence of pointers
• Semantical analysis of the logic of bunched implications
• An algebraic glimpse at bunched implications and separation logic
• Linear resources in Isabelle/HOL
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
• A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories
• Day algebras
• Equivalence and conditional independence in atomic sheaf logic
• Safety, relative tightness and the probabilistic frame rule
• From IF to BI. A tale of dependence and separation
• A calculus and logic of bunched resources and processes
• Algebra and logic for access control
• Graphical models of separation logic

This page was built for publication: Possible worlds and resources: The semantics of \(\mathbf{BI}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1826634)