On models of higher-order separation logic

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.