局部局部推理：一种全地面存储的BI-超规则
Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store
摘要：
关于动态内存分配的建模和推理是理论计算机科学的一个完善的分支，其作为语义、推理和证明理论中臭名昭著的挑战的来源而特别著名。我们利用最近取得的进展全地面存储的范畴语义，在一个完整的地面存储单子，建立一个相应的语义的高阶逻辑在相应的程序。我们的主要结果是一个（直觉主义）BI-hyperdoctrine，这可以说是本地存储的高阶逻辑的语义核心的建设。虽然我们已经广泛使用了现有的通用工具，但必须进行某些原则性的更改才能实现所需的构造：虽然原始的monad适用于全部堆（禁用悬挂指针），但我们的版本涉及部分堆（heaplet），以使用分离合取来实现组合推理。我们的建设的另一个显着特点是，在现有的通用方法相比，我们的BI-代数不直接源于内部的范畴部分交换幺半群。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
