Classical BI

DOI10.1145/1480881.1480923MaRDI QIDQ5261530zbMATH OpenOpenAlexFDO

Authors James Brotherston, Cristiano Calcagno

Publication date 3 July 2015

Published in Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1480881.1480923

zbMATH Keywords

bunched implicationsclassical BIcompletenesscut-eliminationdisplay logicresource modelssemantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Classical BI: Its Semantics and Proof Theory
• A modal BI logic for dynamic resource properties
• scientific article; zbMATH DE number 2051381
• Reasoning about resources and information: a linear logic approach
• The semantics of BI and resource tableaux
• A modal separation logic for resource dynamics
• scientific article; zbMATH DE number 7307099
• Bi-intuitionistic logics: a new instance of an old problem
• scientific article; zbMATH DE number 638618
• Resource separation in dynamic logic of propositional assignments

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
• Classical BI: Its Semantics and Proof Theory
• On Model Checking Boolean BI
• scientific article; zbMATH DE number 2051381 (Why is no real title available?)
• The virtues of idleness: a decidable fragment of resource agent logic

This page was built for publication: Classical BI

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