Hoare triples mediate between logic and computation, so their interpretation plays a key role in the semantics of separation logic. Modern separation logics express their Hoare triples in terms of a weakest precondition modality. Often, the most difficult part of developing a separation logic is finding a weakest precondition modality that is computationally adequate in an appropriate sense while still supporting compositional proof rules. In the presence of effects and resources, there is often no canonical choice for the weakest precondition modality, but the design space for these modalities remains underexplored. Existing theoretical work on separation logic concentrates on the logic of bunched implications (BI) and its higher-order extensions, while theoretical studies of weakest preconditions have only dealt with structural logics.

In this work-in-progress talk, we attempt to provide a theory of weakest preconditions for separation logics by viewing them as liftings of a monad T from a category of types C to a category of predicates C’ fibered over C. Our approach follows Aguirre and Katsumata [1], who developed a theory of structural weakest preconditions in terms of monad liftings. We test our new approach by exhibiting a standard separation logic for heap-manipulating programs as a monad lifting. We will also describe a construction for obtaining new monad liftings from old.