Fibered Separation Logic: Weakest Preconditions, Universal Constructions, and Local Independence

Abstract

This paper introduces a categorical framework for models of higher-order separation logic including the weakest precondition modality. Weakest preconditions are interpreted by strong monads on a category fibered over a model of Moggi's computational lambda calculus. The fibered categories in question are termed bunched fibrations and shown to be equivalent to BI hyperdoctrines. Well-known heuristic techniques for obtaining weakest preconditions are shown to be expressible in categorical terms and are proved sound. The ``baking in the frame rule'' trick is shown to satisfy a universal property. Constructions are given for extending a program logic with cost credits. Our largest case study is parametrized by a category having local independent product (LIP) structure, a notion due to Simpson that axiomatizes name generation, randomness, and local state. From an LIP category, we construct an allocation monad, a bunched fibration, and a monad lifting. We instantiate our construction to obtain a novel probabilistic separation logic for measure-theoretic probability that both simplifies and clarifies prior work.

arXiv comment41 pages, 5 figures