Classical BI: Its Semantics and Proof Theory

DOI10.2168/LMCS-6(3:3)2010MaRDI QIDQ3575307zbMATH OpenFDO

Authors James Brotherston, Cristiano Calcagno

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)

Recommendations

• Proof-theoretic semantics for classical mathematics
• Bialgebraic semantics for logic programming
• scientific article; zbMATH DE number 5920146
• Bisimulation and propositional intuitionistic logic
• Bilattices and the semantics of logic programming
• Classical BI
• scientific article; zbMATH DE number 638618
• A proof-theoretic study of bi-intuitionistic propositional sequent calculus
• Classical logic, continuation semantics and abstract machines
• Bisimulations and predicate logic

Cited in

(22)

• A Games Model of Bunched Implications
• Bunched sequential information
• scientific article; zbMATH DE number 638618 (Why is no real title available?)
• Focused proof-search in the logic of bunched implications
• Ribbon proofs
• Weakening Relation Algebras and FL$$^2$$-algebras
• Stone-type dualities for separation logics
• Abstract hidden Markov models: a monadic account of quantitative information flow
• Effect algebras, presheaves, non-locality and contextuality
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Effect algebras, presheaves, non-locality and contextuality
• A stone-type duality theorem for separation logic via its underlying bunched logics
• Undecidability of propositional separation logic and its neighbours
• Effect algebras, Girard quantales and complementation in separation logic
• The semantics and proof theory of the logic of bunched implications
• An algebraic glimpse at bunched implications and separation logic
• Relating labelled and label-free bunched calculi in BI logic
• A unified display proof theory for bunched logic
• Bunched logics displayed
• Classical BI
• A comparison between monoidal and substructural logics
• An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics

Describes a project that uses

Uses Software

• jStar

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

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