A denotationally-based program logic for higher-order store
Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal
TL;DR
The paper develops Tulip, a denotational, higher-order separation logic for reasoning about higher-order store with general references and polymorphism. It achieves this by leveraging impredicative guarded dependent type theory to model semantic worlds and store, producing a BI-hyperdoctrine that supports persistence, the later modality, and weakest preconditions, while ensuring soundness. A key contribution is proving Tulip’s soundness against its denotational model and demonstrating equational reasoning that can replace head-reduction-focused proofs in traditional logics, as illustrated by a linked-list append case study. The work positions Tulip as a modular, foundations-grounded alternative to operational logics like Iris, with potential extensions to ghost state and concurrency, and discusses future implementation and refinement avenues.
Abstract
Separation logic is used to reason locally about stateful programs. State of the art program logics for higher-order store are usually built on top of untyped operational semantics, in part because traditional denotational methods have struggled to simultaneously account for general references and parametric polymorphism. The recent discovery of simple denotational semantics for general references and polymorphism in synthetic guarded domain theory has enabled us to develop TULIP, a higher-order separation logic over the typed equational theory of higher-order store for a monadic version of System F{mu,ref}. The Tulip logic differs from operationally-based program logics in two ways: predicates range over the meanings of typed terms rather than over the raw code of untyped terms, and they are automatically invariant under the equational congruence of higher-order store, which applies even underneath a binder. As a result, "pure" proof steps that conventionally require focusing the Hoare triple on an operational redex are replaced by a simple equational rewrite in Tulip. We have evaluated Tulip against standard examples involving linked lists in the heap, comparing our abstract equational reasoning with more familiar operational-style reasoning. Our main result is the soundness of Tulip, which we establish by constructing a BI-hyperdoctrine over the denotational semantics of F{mu,ref} in an impredicative version of synthetic guarded domain theory.