Classical BI: Its Semantics and Proof Theory

DOI10.2168/LMCS-6(3:3)2010zbMath1198.03028MaRDI QIDQ3575307

Cristiano Calcagno, James Brotherston

Publication date: 27 July 2010

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

completenessdisplay logicbunched logicbunched implicationclassical BIresource models

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Related Items (13)

A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ Effect Algebras, Presheaves, Non-locality and Contextuality ⋮ An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics ⋮ Effect algebras, presheaves, non-locality and contextuality ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ A comparison between monoidal and substructural logics ⋮ Weakening Relation Algebras and FL$$^2$$-algebras ⋮ Bunched logics displayed ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Effect algebras, Girard quantales and complementation in separation logic ⋮ Focused proof-search in the logic of bunched implications ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• jStar

This page was built for publication: Classical BI: Its Semantics and Proof Theory