Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding

DOI10.1017/S0960129509007567MaRDI QIDQ3636908zbMATH OpenFDO

Authors Dominique Larchey-Wendling, Didier Galmiche

Publication date 30 June 2009

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129509007567

zbMATH Keywords

Kripke semanticslogic of bunched implicationsseparation logicspatial logictableau proof system

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Expressivity Properties of Boolean BI Through Relational Models
• The semantics and proof theory of the logic of bunched implications
• The Logic of Bunched Implications
• Temporal BI: proof system, semantics and translations
• On Model Checking Boolean BI

Cites work

• A calculus and logic of resources and processes
• Anytime, anywhere: modal logics for mobile ambients
• BI as an assertion language for mutable data structures
• Context logic as modal logic, completeness and parametric inexpressivity
• Deciding validity in a spatial logic for trees
• Elimination of quantifiers and undecidability in spatial logics for concurrency
• Intuitionistic propositional logic is polynomial-space complete
• Models and Separation Logics for Resource Trees
• On the Almighty Wand
• Semantic Labelled Tableaux for Propositional BI
• Systems modelling via resources and processes: philosophy, calculus, semantics, and logic
• The semantics of BI and resource tableaux

Cited in

(7)

• Bunched logics displayed
• A unified display proof theory for bunched logic
• An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
• Completeness for a first-order abstract separation logic
• Bringing Order to the Separation Logic Jungle
• Expressivity Properties of Boolean BI Through Relational Models
• An algebraic glimpse at bunched implications and separation logic

This page was built for publication: Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding

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