Possible worlds and resources: The semantics of BI

DOI10.1016/J.TCS.2003.11.020zbMATH Open1055.03021DBLPjournals/tcs/PymOY04OpenAlexW2013474929WikidataQ56445145 ScholiaQ56445145MaRDI QIDQ1826634FDOQ1826634

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

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

zbMATH Keywords

logic of bunched implicationspossible-worlds semanticslogic of resources

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)

Cites Work

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

Cited In (52)

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

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)