Aarhus University Seal / Aarhus Universitets segl

Nested hoare triples and frame rules for higher-order store

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Jan Schwinghammer, Saarland University, Germany
  • Lars Birkedal
  • Bernhard Reus, University of Sussex, United Kingdom
  • Hongseok Yang, Queen Mary University of London, United Kingdom

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 combination of rules can be shown consistent by means of a Kripke model where worlds live in a recursively defined ultrametric space. The resulting logic allows us to elegantly prove programs involving stored code. In particular, it leads to natural specifications and proofs of invariants required for dealing with recursion through the store.

Original languageEnglish
Title of host publicationComputer Science Logic : 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings
EditorsErich Grädel, Reinhard Kahle
Number of pages15
PublisherSpringer
Publication year2 Nov 2009
Pages440-454
ISBN (print)9783642040269
ISBN (Electronic)978-3-642-04027-6
DOIs
Publication statusPublished - 2 Nov 2009
Externally publishedYes
SeriesLecture Notes in Computer Science
Volume5771
ISSN0302-9743

See relations at Aarhus University Citationformats

ID: 81389201