A denotationally-based program logic for higher-order store

Separation logic is used to reason locally about stateful programs. State ofthe art program logics for higher-order store are usually built on top ofuntyped operational semantics, in part because traditional denotational methodshave struggled to simultaneously account for general references and parametricpolymorphism. The recent discovery of simple denotational semantics for generalreferences and polymorphism in synthetic guarded domain theory has enabled usto develop TULIP, a higher-order separation logic over the typed equationaltheory of higher-order store for a monadic version of System F{mu,ref}. TheTulip logic differs from operationally-based program logics in two ways:predicates range over the meanings of typed terms rather than over the raw codeof untyped terms, and they are automatically invariant under the equationalcongruence of higher-order store, which applies even underneath a binder. As aresult, "pure" proof steps that conventionally require focusing the Hoaretriple on an operational redex are replaced by a simple equational rewrite inTulip. We have evaluated Tulip against standard examples involving linked listsin the heap, comparing our abstract equational reasoning with more familiaroperational-style reasoning. Our main result is the soundness of Tulip, whichwe establish by constructing a BI-hyperdoctrine over the denotational semanticsof F{mu,ref} in an impredicative version of synthetic guarded domain theory.Comment: To appear in proceedings of MFPS 202