BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Parametric completeness for separation theories (v
ia hybrid logic) - James Brotherston\, University
College London
DTSTART:20131018T150000Z
DTEND:20131018T160000Z
UID:TALK1191AT
URL:/talk/index/1191
DESCRIPTION:In this talk\, we consider the logical gap between
the following two concepts: \n\n(1) **provabilit
y in a propositional axiomatisation** of separat
ion logic\, which is usually given by the bunched
logic BBI\; and \n\n(2) **validity in an intended
class of models** of separation logic\, as comm
only considered in its program verification applic
ations. Such intended classes are usually specifie
d by a collection of algebraic axioms describing s
pecific model properties\, which we call a **sepa
ration theory**. \n\nHere\, we show first that s
everal typical properties of separation theories a
re in fact **not definable** in BBI. Then\, we
show that these properties become definable in a n
atural **hybrid extension** of BBI\, obtained b
y adding a theory of **naming** to BBI in the s
ame way that hybrid logic extends normal modal log
ic. Finally\, we show how to build an axiomatic pr
oof system for our hybrid logic in such a way that
adding any axiom of a certain form yields a sound
and complete proof system with respect to the mod
els satisfying those axioms. In particular\, this
yields sound and complete proof systems for any se
paration theory from our considered class (which\,
to the best of our knowledge\, includes all those
appearing in the literature). \n\nThis is joint w
ork with Jules Villard\, also at UCL.
LOCATION:UG10 Learning Centre
CONTACT:Paul Levy
END:VEVENT
END:VCALENDAR