A denotationally-based program logic for higher-order store

TL;DR

This paper introduces TULIP, a denotational higher-order separation logic for reasoning about higher-order store in typed functional languages, enabling equational reasoning and invariance under store transformations.

Contribution

It develops TULIP, a novel denotational program logic for higher-order store that overcomes limitations of operational semantics and supports invariant reasoning under equational theory.

Findings

TULIP is sound for higher-order store reasoning.

It simplifies proofs by replacing redex focusing with equational rewrites.

TULIP effectively handles linked list examples in the heap.

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.