Sciweavers

Share
POPL
2007
ACM

Context logic as modal logic: completeness and parametric inexpressivity

9 years 5 months ago
Context logic as modal logic: completeness and parametric inexpressivity
Separation Logic, Ambient Logic and Context Logic are based on a similar style of reasoning about structured data. They each consist of a structural (separating) composition for reasoning about disjoint subdata, and corresponding structural adjoint(s) for reasoning hypothetically about data. We show how to interpret these structural connectives as modalities in Modal Logic and prove completeness results. The structural connectives are essential for describing properties of the underlying data, such as weakest preconditions for Hoare reasoning for Separation and Context Logic, and security properties for Ambient Logic. In fact, we introduced Context Logic to reason about tree update, precisely because the structural connectives of the Ambient Logic did not have enough expressive power. Despite these connectives being essential, first Lozes then Dawar, Gardner and Ghelli proved elimination results for Separation Logic and Ambient Logic (without quantifiers). In this paper, we solve this...
Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Cristiano Calcagno, Philippa Gardner, Uri Zarfaty
Comments (0)
books