The semantics and proof theory of the logic of bunched implications

zbMATH Open1068.03001MaRDI QIDQ2487871FDOQ2487871

Authors: David Pym 

Publication date: 11 August 2005

Published in: Applied Logic Series (Search for Journal in Brave)

Recommendations

• The Logic of Bunched Implications
• scientific article; zbMATH DE number 1231702
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Classical BI: Its Semantics and Proof Theory
• Bunched logics displayed

zbMATH Keywords

proof theoryintuitionistic logiclinear logicmodel theorylogic of bunched implicationscomputational interpretations

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30)

Cited In (61)

• Birkhoff's and Mal'cev's theorems for implicational tonoid logics
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
• An algebraic glimpse at bunched implications and separation logic
• Separation Logic Tutorial
• An epistemic separation logic with action models
• The logic of separation logic: models and proofs
• A separation logic with histories of epistemic actions as resources
• Title not available (Why is that?)
• A public announcement separation logic
• Title not available (Why is that?)
• Bunched sequential information
• Logical consequence and the paradoxes
• Temporal BI: proof system, semantics and translations
• Focused proof-search in the logic of bunched implications
• Weakening Relation Algebras and FL$$^2$$-algebras
• Ribbon proofs
• Algebra and logic for access control
• Separation logics and modalities: a survey
• Join-completions of partially ordered algebras
• A calculus and logic of resources and processes
• Exponential-size model property for PDL with separating parallel composition
• Tableaux methods for propositional dynamic logics with separating parallel composition
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Pseudo-distributive laws and axiomatics for variable binding
• Logic for Programming, Artificial Intelligence, and Reasoning
• From IF to BI. A tale of dependence and separation
• On temporal and separation logics
• Abstract syntax: substitution and binders
• Semantical analysis of the logic of bunched implications
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Footprints in Local Reasoning
• On Model Checking Boolean BI
• Undecidability of propositional separation logic and its neighbours
• Inconsistency-tolerant bunched implications
• Two cotensors in one: presentations of algebraic theories for local state and fresh names
• Separation Logic Semantics for Communicating Processes
• Kripke Resource Models of a Dependently-typed, Bunched  -calculus
• Title not available (Why is that?)
• Automated theorem proving by resolution in non-classical logics
• Expressing second-order sentences in intuitionistic dependence logic
• The Lambek calculus extended with intuitionistic propositional logic
• On the construction of free algebras for equational systems
• Fine-grained concurrency with separation logic
• An epistemic separation logic
• Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
• The structure of generalized BI-algebras and weakening relation algebras
• Lewis meets Brouwer: constructive strict implication
• On Composing Finite Forests with Modal Logics
• Modal algebra and Petri nets
• Algebra and logic for resource-based systems modelling
• Coordination: Reo, Nets, and Logic
• A unified display proof theory for bunched logic
• Bunched logics displayed
• Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm \textsf{PEARL}
• Title not available (Why is that?)
• Distributive residuated frames and generalized bunched implication algebras
• Local reasoning about data update
• Relation algebras, idempotent semirings and generalized bunched implication algebras
• An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
• Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
• A Games Model of Bunched Implications

This page was built for publication: The semantics and proof theory of the logic of bunched implications

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