论文标题
当地的当地推理：全地面商店的双重旋转
Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store
论文作者
论文摘要
关于动态记忆分配的建模和推理是理论计算机科学的良好链，它在语义，推理和证明理论中尤其是臭名昭著的挑战来源。就完整的地面商店单元而言，我们利用了全面商店的分类语义的最新进展，以在相应的程序上构建高阶逻辑的相应语义。我们的主要结果是建造（直觉的）双重旋转，这可以说是当地商店上高阶逻辑的语义核心。尽管我们已经广泛使用了现有的通用工具，但必须进行某些原则上的更改才能实现所需的结构：虽然原始的单子在总堆（禁用悬挂的指针）上起作用，但我们的版本涉及部分堆（堆堆）以启用使用分离连词的组成推理。我们构造的另一个显着特征是，与现有的通用方法相反，我们的双向代数并非直接源于内部分类部分交换性单体。
Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory. We capitalize on recent progress on categorical semantics of full ground store, in terms of a full ground store monad, to build a corresponding semantics of a higher order logic over the corresponding programs. Our main result is a construction of an (intuitionistic) BI-hyperdoctrine, which is arguably the semantic core of higher order logic over local store. Although we have made an extensive use of the existing generic tools, certain principled changes had to be made to enable the desired construction: while the original monad works over total heaps (to disable dangling pointers), our version involves partial heaps (heaplets) to enable compositional reasoning using separating conjunction. Another remarkable feature of our construction is that, in contrast to the existing generic approaches, our BI-algebra does not directly stem from an internal categorical partial commutative monoid.
