Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1275497.1275499 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
additional key words and phrases: separation logic,higher-order separation logic,earlier correspondence,data abstraction,simple notion,abstraction,sound reasoning principle,precise correspondence,propositional bi,bi hyperdoctrine,higher-order predicate,predicate bi,separation logic,hyperdoctrines,higher order | Separation logic,Predicate variable,Computer science,Propositional calculus,Theoretical computer science,Predicate functor logic,Predicate logic,Dynamic logic (modal logic),Intermediate logic,Higher-order logic | Journal |
Volume | Issue | ISSN |
29 | 5 | 0164-0925 |
Citations | PageRank | References |
31 | 1.51 | 23 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| L. Birkedal | 1 | 88 | 4.45 |
| Lars Birkedal | 2 | 1481 | 96.84 |
| Noah Torp-smith | 3 | 122 | 6.74 |