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-超范畴来建立。