Journal article icon

Journal article

Nested Hoare Triples and Frame Rule for Higher−order Store

Abstract:

Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several variations of higher-order frame rules.

The interaction of nested triples and frame rules can be subtle, and the inclusion of certain frame rules is in fact unsound. A particular combinatio...

Expand abstract

Actions


Access Document


Files:

Authors


Journal:
Logical Methods in Computer Science
Volume:
7(3:21)
Publication date:
2011-01-01
URN:
uuid:c8699ee5-5825-4782-a8d8-34c0de95c123
Local pid:
cs:4985

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP