James Brotherston ; Cristiano Calcagno - Classical BI: Its Semantics and Proof Theory

lmcs:1014 - Logical Methods in Computer Science, July 20, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:3)2010
Classical BI: Its Semantics and Proof Theory

Authors: James Brotherston ; Cristiano Calcagno

    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 in particular a multiplicative version of classical negation). At the semantic level, CBI-formulas have the normal bunched logic reading as declarative statements about resources, but its resource models necessarily feature more structure than those for other bunched logics; principally, they satisfy the requirement that every resource has a unique dual. At the proof-theoretic level, a very natural formalism for CBI is provided by a display calculus à la Belnap, which can be seen as a generalisation of the bunched sequent calculus for BI. In this paper we formulate the aforementioned model theory and proof theory for CBI, and prove some fundamental results about the logic, most notably completeness of the proof theory with respect to the semantics.

    Volume: Volume 6, Issue 3
    Published on: July 20, 2010
    Accepted on: June 25, 2015
    Submitted on: August 1, 2009
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    Linked data

    Source : ScholeXplorer References DOI 10.1145/1988042.1988050
    Source : ScholeXplorer References DOI 10.1145/360204.375719
    Source : ScholeXplorer References DOI 10.1145/373243.375719
    • 10.1145/373243.375719
    • 10.1145/373243.375719
    • 10.1145/373243.375719
    • 10.1145/1988042.1988050
    • 10.1145/360204.375719
    • 10.1145/360204.375719
    • 10.1145/360204.375719
    BI as an assertion language for mutable data structures
    Samin Ishtiaq ; Peter W. O'Hearn ;

    15 Documents citing this article


    Consultation statistics

    This page has been seen 371 times.
    This article's PDF has been downloaded 366 times.