![]() |
![]() |
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
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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Theoretical computer science seminar Aerospace Seminar SeriesOther talksCounting cycles in planar graphs Life : it’s out there, but what and why ? TBA Control variates for computing transport coefficients TBA Wave turbulence in the Schrödinger-Helmholtz equation |