Classical BI: Its Semantics and Proof Theory
We present Classical BI (CBI), a new addition to the family of bunched logics which originates in O'Hearn and Pym's logic of bunched implications BI. CBI differs from existing bunched logics in that its multiplicative connectives behave classically rather than intuitionistically (including...
Main Authors: | James Brotherston, Cristiano Calcagno |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2010-07-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/1014/pdf |
Similar Items
-
Intuitionistic Layered Graph Logic: Semantics and Proof Theory
by: Simon Docherty, et al.
Published: (2018-10-01) -
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
by: Robert Constable, et al.
Published: (2008-09-01) -
On the strength of proof-irrelevant type theories
by: Benjamin Werner
Published: (2008-09-01) -
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
by: Andreas Abel, et al.
Published: (2011-05-01) -
Some model theory for the modal $\mu$-calculus: syntactic characterisations of semantic properties
by: Gaëlle Fontaine, et al.
Published: (2018-02-01)