The semantics and proof theory of the logic of bunched implications

MaRDI QIDQ2487871zbMATH OpenFDO

Authors David Pym

Publication date 11 August 2005

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

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)

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

Cited in

(68)

• A Games Model of Bunched Implications
• Bunched sequential information
• scientific article; zbMATH DE number 1424038 (Why is no real title available?)
• Logical consequence and the paradoxes
• A public announcement separation logic
• scientific article; zbMATH DE number 7204446 (Why is no real title available?)
• Temporal BI: proof system, semantics and translations
• Focused proof-search in the logic of bunched implications
• Ribbon proofs
• Algebra and logic for access control
• Weakening Relation Algebras and FL^2-algebras
• Join-completions of partially ordered algebras
• Separation logics and modalities: a survey
• A calculus and logic of resources and processes
• Pseudo-distributive laws and axiomatics for variable binding
• Exponential-size model property for PDL with separating parallel composition
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Tableaux methods for propositional dynamic logics with separating parallel composition
• A complete axiomatisation for quantifier-free separation logic
• Birkhoff's and Mal'cev's theorems for implicational tonoid logics
• From IF to BI. A tale of dependence and separation
• Logic for Programming, Artificial Intelligence, and Reasoning
• On temporal and separation logics
• Abstract syntax: substitution and binders
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Semantical analysis of the logic of bunched implications
• Footprints in Local Reasoning
• Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions
• On Model Checking Boolean BI
• Undecidability of propositional separation logic and its neighbours
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
• Two-dimensional Kripke semantics. II: Stability and completeness
• Inferentialist resource semantics
• Inconsistency-tolerant bunched implications
• Two cotensors in one: presentations of algebraic theories for local state and fresh names
• Separation Logic Semantics for Communicating Processes
• Expressing second-order sentences in intuitionistic dependence logic
• Automated theorem proving by resolution in non-classical logics
• Kripke Resource Models of a Dependently-typed, Bunched  -calculus
• The Lambek calculus extended with intuitionistic propositional logic
• scientific article; zbMATH DE number 614413 (Why is no real title available?)
• On the construction of free algebras for equational systems
• Entanglement of sections: the pushout of entangled and parameterized quantum information
• Fine-grained concurrency with separation logic
• An epistemic separation logic
• An algebraic glimpse at bunched implications and separation logic
• Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
• The structure of generalized BI-algebras and weakening relation algebras
• Separation Logic Tutorial
• Internal and external calculi: ordering the jungle without being lost in translations
• Lewis meets Brouwer: constructive strict implication
• Modal algebra and Petri nets
• On Composing Finite Forests with Modal Logics
• 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}
• First-order hybrid separation logic
• Distributive residuated frames and generalized bunched implication algebras
• An epistemic separation logic with action models
• Local reasoning about data update
• The logic of separation logic: models and proofs
• The quantum monadology
• An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
• Relation algebras, idempotent semirings and generalized bunched implication algebras
• A separation logic with histories of epistemic actions as resources
• Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding

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)