Separation Logic for Higher-Order Store

DOI10.1007/11874683_38MaRDI QIDQ3613364zbMATH OpenOpenAlexFDO

Authors Bernhard Reus, Jan Schwinghammer

Publication date 12 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11874683_38

Mathematics Subject Classification ID

Data structures (68P05) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Automata, Languages and Programming
• Hoare logic for higher order store using simple semantics
• A categorical semantics of higher order store
• Separation logic for high-level synthesis
• Bringing Order to the Separation Logic Jungle
• Separation logic and abstraction
• Separation logic and concurrency
• The essence of higher-order concurrent separation logic

Cited in

(35)

• Nested Hoare Triples and Frame Rules for Higher-Order Store
• Automated theorem proving for assertions in separation logic with all connectives
• Connecting higher-order separation logic to a first-order outside world
• Relational Parametricity and Separation Logic
• Relative Store Fragments for Singleton Abstraction
• False failure: creating failure models for separation logic
• Separation logic and abstraction
• Separation logic style reasoning in a refinement based language
• Extended transitive separation logic
• Symbolic execution proofs for higher order store programs
• The relationship between separation logic and implicit dynamic frames
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• A proof system for separation logic with magic wand
• Local reasoning for global graph properties
• Weak updates and separation logic
• Extending separation logic with fixpoints and postponed substitution
• Mechanized verification with sharing
• Algebraic Methodology and Software Technology
• Fictional separation logic
• Nested Hoare triples and frame rules for higher-order store
• Higher-order separation logic in Isabelle/HOLCF
• Separation logic modulo theories
• Unifying separation logic and region logic to allow interoperability
• Logical Reasoning for Higher-Order Functions with Local State
• Syntactic control of interference for separation logic
• A Simple Model of Separation Logic for Higher-Order Store
• Separation Logic Tutorial
• Programming Languages and Systems
• Separation logic for non-local control flow and block scope variables
• High-level separation logic for low-level code
• Relational Parametricity and Separation Logic
• The relationship between separation logic and implicit dynamic frames
• Local local reasoning: a BI-hyperdoctrine for full ground store
• Types, Maps and Separation Logic

This page was built for publication: 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 Q3613364)