Search

• < Previous
• 1
• Next >

Nested Hoare Triples and Frame Rules for Higher-order Store

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&nbsp;[&hellip;]