Brotherston, J;
Villard, J;
(2014)
Parametric completeness for separation theories.
ACM SIGPLAN Notices
, 49
(1)
453 - 464.
10.1145/2535838.2535844.
![[thumbnail of p453-brotherston.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) |
PDF
p453-brotherston.pdf Download (662kB) |
Abstract
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(#) 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.
| Type: | Article |
|---|---|
| Title: | Parametric completeness for separation theories |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/2535838.2535844 |
| Publisher version: | http://dx.doi.org/10.1145/2535838.2535844 |
| Language: | English |
| Additional information: | Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). Copyright is held by the author/owner(s). |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1421933 |
Archive Staff Only
 |
View Item |
