A Simple Model of Separation Logic for Higher-Order Store

DOI10.1007/978-3-540-70583-3_29MaRDI QIDQ3519513zbMATH OpenOpenAlexFDO

Authors Bernhard Reus, Hongseok Yang, Lars Birkedal, Jan Schwinghammer

Publication date 19 August 2008

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70583-3_29

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Separation Logic for Higher-Order Store
• Automata, Languages and Programming
• Nested Hoare triples and frame rules for higher-order store
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Hoare logic for higher order store using simple semantics

Cited in

(9)

• Specification patterns for reasoning about recursion through the store
• Nested Hoare Triples and Frame Rules for Higher-Order Store
• A theory of indirection via approximation
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Hoare logic for higher order store using simple semantics
• Nested Hoare triples and frame rules for higher-order store
• Step-indexed Kripke model of separation logic for storable locks
• Programming Languages and Systems
• High-level separation logic for low-level code

This page was built for publication: A Simple Model of Separation Logic for Higher-Order Store

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3519513)