University of Birmingham > Talks@bham > Theoretical computer science seminar > Parametric completeness for separation theories (via hybrid logic)

Parametric completeness for separation theories (via hybrid logic)

Add to your list(s) Download to your calendar using vCal

  • UserJames Brotherston, University College London
  • ClockFriday 18 October 2013, 16:00-17:00
  • HouseUG10 Learning Centre.

If you have a question about this talk, please contact Paul Levy.

In this talk, we consider the logical gap between the following two concepts:

(1) provability in a propositional axiomatisation of separation logic, which is usually given by the bunched logic BBI ; and

(2) validity in an intended class of models of separation logic, as commonly considered in its program verification applications. Such intended classes are usually specified by a collection of algebraic axioms describing specific model properties, which we call a separation theory.

Here, we show first that several typical properties of separation theories are in fact not definable in BBI . Then, we show that these properties become definable in a natural hybrid extension of BBI , obtained by adding a theory of naming to BBI in the same way that hybrid logic extends normal modal logic. Finally, we show how to build an axiomatic proof 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 models satisfying those axioms. In particular, this yields sound and complete proof systems for any separation theory from our considered class (which, to the best of our knowledge, includes all those appearing in the literature).

This is joint work with Jules Villard, also at UCL .

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.