BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Deciding Boolean BI (via Display Logic) - James Brotherston\,  Imp
 erial College London
DTSTART:20090306T140000Z
DTEND:20090306T150000Z
UID:TALK17063@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:In the logic of bunched implications BI\, one can choose to\ni
 nterpret the additive connectives as behaving either\nintuitionistically o
 r classically.  Boolean BI (BBI)\, obtained\nby making the latter choice\,
  forms the basis of separation logic\nand most of the related program anal
 ysis applications. Yet\, in\ncontrast to its intuitionistic counterpart\, 
 the proof theory of\nBBI is (to our knowledge) almost entirely absent in t
 he literature\nand its decidability has hitherto been unknown.\n\nIn this 
 talk\, we give a display calculus proof system for BBI\nbased on Belnap's 
 general display logic. We show that\ncut-elimination holds in our system a
 nd that it is sound and\ncomplete with respect to the usual notion of vali
 dity for BBI.\nWe then demonstrate that proof search in the system can be\
 nrestricted to a finitely bounded space (without loss of\ngenerality). Thu
 s provability in our display calculus is\ndecidable\, and consequently so 
 too is validity in BBI.\n\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR