BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Classical BI (A Logic for Reasoning About Dualising Resource) - Ja
 mes Brotherston\, Imperial College
DTSTART:20081010T130000Z
DTEND:20081010T140000Z
UID:TALK13031@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:We show how to extend O'Hearn and Pym's logic of bunched\nimpl
 ications\, BI\, to classical BI (CBI)\, in which both the\nadditive and th
 e multiplicative connectives behave classically.\nSpecifically\, CBI is a 
 non-conservative extension of\n(propositional) boolean BI that includes mu
 ltiplicative\nversions of falsity\, negation and disjunction.  We give an\
 nalgebraic semantics for CBI that leads us naturally to consider\nresource
  models of CBI in which every resource has a unique\ndual.  We then give a
  cut-eliminating proof system for CBI\,\nbased on Belnap's display logic\,
  and demonstrate soundness and\ncompleteness of this proof system with res
 pect to our\nsemantics.\n\n(Joint work with  Cristiano Calcagno)
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR