Séminaire des équipes de recherche
Parametric completeness for separation theories (via hybrid logic)
- Date : 11/09/2013
- Lieu : Inria Paris - Rocquencourt, Amphithéâtre Alan Turing - bâtiment 01
- Intervenant(s) : Jules Villard
- Organisateur(s) : Gallium
In this talk, we consider the logical gap between the following two concepts:
- *provability in some propositional axiomatisation* of separation logic, which is usually given by the bunched logic BBI; and
- *validity in an intended class of models* of separation logic, as commonly considered in its program verification applications.
An intended class of separation models is usually specified by a collection of algebraic axioms describing the specific model properties that are expected to hold, which we call a *separation theory*. It is well known that BBI is incomplete for many such separation theories.
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 James Brotherston, also at UCL.