BI-hyperdoctrines, higher-order separation logic, and abstraction
BI-hyperdoctrines, higher-order separation logic, and abstraction
复制标题
DOI：
10.1145/1275497.1275499
复制
发表时间：
2007-01-01
影响因子：
1.3
通讯作者：
Torp-Smith, Noah
中科院分区：
文献类型：
--
作者：
Biering, Bodil;Birkedal, Lars;Torp-Smith, Noah
我们提出了分离逻辑和谓词BI的简单概念之间的精确对应关系，从而扩展了分离逻辑和命题BI之间给出的早期对应关系。此外，我们介绍了BI HyperDoctrine的概念，表明它可以很好地建模古典和直觉的第一和高级谓词BI，并使用它来表明我们可以轻松地将分离逻辑扩展到高阶。我们还证明，此扩展对于程序证明很重要，因为它在存在混叠的情况下为数据抽象提供了合理的推理原则。
We present a precise correspondence between separation logic and a simple notion of predicate BI, extending the earlier correspondence given between part of separation logic and propositional BI. Moreover, we introduce the notion of a BI hyperdoctrine, show that it soundly models classical and intuitionistic first- and higher-order predicate BI, and use it to show that we may easily extend separation logic to higher-order. We also demonstrate that this extension is important for program proving, since it provides sound reasoning principles for data abstraction in the presence of aliasing.