The semantics and proof theory of the logic of bunched implications

zbMath1068.03001MaRDI QIDQ2487871

David J. Pym

Publication date: 11 August 2005

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

zbMATH Keywords

linear logicmodel theoryproof theoryintuitionistic logiclogic 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) Categorical logic, topoi (03G30) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (49)

Bunched sequential information ⋮ On Composing Finite Forests with Modal Logics ⋮ Relation Algebras, Idempotent Semirings and Generalized Bunched Implication Algebras ⋮ From IF to BI. A tale of dependence and separation ⋮ Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition ⋮ A Unified Display Proof Theory for Bunched Logic ⋮ An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics ⋮ Automated theorem proving by resolution in non-classical logics ⋮ Pseudo-distributive laws and axiomatics for variable binding ⋮ A calculus and logic of resources and processes ⋮ The Lambek calculus extended with intuitionistic propositional logic ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ Exponential-Size Model Property for PDL with Separating Parallel Composition ⋮ Temporal BI: proof system, semantics and translations ⋮ An Epistemic Separation Logic ⋮ Separation logics and modalities: a survey ⋮ Weakening Relation Algebras and FL$$^2$$-algebras ⋮ Distributive residuated frames and generalized bunched implication algebras ⋮ Bunched logics displayed ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Semantical analysis of the logic of bunched implications ⋮ An epistemic separation logic with action models ⋮ A separation logic with histories of epistemic actions as resources ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras via an implementation of the algorithm \textsf{PEARL} ⋮ Expressing second-order sentences in intuitionistic dependence logic ⋮ A public announcement separation logic ⋮ Logical consequence and the paradoxes ⋮ Focused proof-search in the logic of bunched implications ⋮ Footprints in Local Reasoning ⋮ Separation Logic Semantics for Communicating Processes ⋮ Join-completions of partially ordered algebras ⋮ Algebra and logic for access control ⋮ Coordination: Reo, Nets, and Logic ⋮ Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names ⋮ Unnamed Item ⋮ On Temporal and Separation Logics ⋮ On the construction of free algebras for equational systems ⋮ Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition ⋮ Algebra and logic for resource-based systems modelling ⋮ Fine-grained concurrency with separation logic ⋮ Possible worlds and resources: The semantics of \(\mathbf{BI}\) ⋮ The structure of generalized BI-algebras and weakening relation algebras ⋮ Separation Logic Tutorial ⋮ Unnamed Item ⋮ Modal algebra and Petri nets ⋮ Local Reasoning about Data Update ⋮ Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic ⋮ Abstract Syntax: Substitution and Binders

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