Output details
11 - Computer Science and Informatics
Imperial College London
Article title
CLASSICAL BI: ITS SEMANTICS AND PROOF THEORY
Type
D - Journal article
Title of journal
Logical Methods in Computer Science
Article number
ARTN 3
Volume number
6
Issue number
3
First page of article
-
ISSN of journal
1860-5974
Year of publication
2010
URL
-
Number of additional authors
1
Additional information
<11>
Classical BI is 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 a multiplicative version of classical negation).
Multiplicative connectives are at the heart of bunched logics, and this paper gives one answer to the long-standing question (since Pym's 2004 monograph) of what it means to negate a resource, showing a number of consistent models where multiplicative negation represents a form of internal duality. Extends paper at POPL'09 22%/160 submissions.
Interdisciplinary
-
Cross-referral requested
-
Research group
E - Programming Languages and Systems
Citation count
1
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
