You are here

A Logic for Reasoning About Dualising Resource

CISA Seminar Series
James Brotherston

We present classical BI (CBI): a nonconservative extension of O'Hearn and Pym's logic of bunched implications, BI, in which both the additive *and* the multiplicative connectives behave classically. In particular, CBI includes multiplicative versions of falsity, negation and disjunction, which are absent in BI. We give an algebraic semantics for CBI that leads us naturally to consider resource models in which every resource has a unique dual. We also give a cut-eliminating proof system for CBI, based on Belnap's display logic, which is sound and complete with respect to our semantics.

This is joint work with Cristiano Calcagno.

Date and time: 
Thursday, 23 October, 2008 - 11:00
60 minutes