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.

翻译：分离逻辑用于局部推理有状态程序。当前针对高阶存储的最先进程序逻辑通常建立在无类型操作语义之上，部分原因在于传统的指称方法难以同时处理通用引用和参数多态性。近期在合成守卫域理论中发现通用引用和多态性的简单指称语义，使我们能够开发TULIP——一种基于带类型等式理论的高阶存储的、针对System F{mu,ref}单子版本的高阶分离逻辑。Tulip逻辑与基于操作的程序逻辑有两方面不同：谓词范围涵盖类型化项的意义而非无类型项的原始代码，且它们在高阶存储的等式同余下自动保持不变——这种同余甚至适用于绑定符之下。因此，传统上需要将霍尔三元组聚焦于操作归约点的"纯"证明步骤，在Tulip中被简单的等式重写所取代。我们针对堆中链表的标准示例对Tulip进行了评估，比较了我们的抽象等式推理与更熟悉的操作风格推理。我们的主要结果是Tulip的可靠性，通过在非谓词版本的合成守卫域理论中为F{mu,ref}的指称语义构建BI-超道义框架予以证明。