In this paper, we close the logical gap between provability in the logic BBI,
which is the propositional basis for separation logic, and validity in an
intended class of separation models, as employed in applications of separation
logic such as program verification. An intended class of separation models is
usually specified by a collection of axioms describing the specific model
properties that are expected to hold, which we call a separation theory.
Our main contributions are as follows. First, we show that several typical
properties of separation theories are not definable in BBI. Second, we show
that these properties become definable in a suitable hybrid extension of BBI,
obtained by adding a theory of naming to BBI in the same way that hybrid logic
extends normal modal logic. The binder-free extension HyBBI captures most of
the properties we consider, and the full extension HyBBI(\downarrow) with the
usual binder of hybrid logic covers all these properties. Third, we present an
axiomatic proof system for our hybrid logic whose extension with any set of
"pure" axioms is sound and complete with respect to the models satisfying those
axioms. As a corollary of this general result, we obtain, in a parametric
manner, a sound and complete axiomatic proof system for any separation theory
from our considered class. To the best of our knowledge, this class includes
all separation theories appearing in the published literature.