Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                        MERCREDI 11 septembre, 10h30

                               -------------
                               Jules Villard
                               -------------

                         University College London

     ==================================================================
     Parametric completeness for separation theories (via hybrid logic)
     ==================================================================

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.