On models of higher-order separation logic
A Bizjak, L Birkedal - Electronic Notes in Theoretical Computer Science, 2018 - Elsevier
Electronic Notes in Theoretical Computer Science, 2018•Elsevier
We show how tools from categorical logic can be used to give a general account of models
of higher-order separation logic with a sublogic of so-called persistent predicates satisfying
the usual rules of higher-order logic. The models of separation logic are based on a notion
of resource, a partial commutative monoid, and the persistent predicates can be defined
using a modality. We classify well-behaved sublogics of persistent predicates in terms of
interior operators on the partial commutative monoid of resources. We further show how the …
of higher-order separation logic with a sublogic of so-called persistent predicates satisfying
the usual rules of higher-order logic. The models of separation logic are based on a notion
of resource, a partial commutative monoid, and the persistent predicates can be defined
using a modality. We classify well-behaved sublogics of persistent predicates in terms of
interior operators on the partial commutative monoid of resources. We further show how the …
Abstract
We show how tools from categorical logic can be used to give a general account of models of higher-order separation logic with a sublogic of so-called persistent predicates satisfying the usual rules of higher-order logic. The models of separation logic are based on a notion of resource, a partial commutative monoid, and the persistent predicates can be defined using a modality. We classify well-behaved sublogics of persistent predicates in terms of interior operators on the partial commutative monoid of resources. We further show how the general constructions can be used to recover the model of Iris, a state-of-the-art higher-order separation logic with guarded recursive predicates.
Elsevier