Nested Hoare Triples and Frame Rules for Higher-Order Store

DOI10.1007/978-3-642-04027-6_32zbMath1257.03056arXiv1109.3031OpenAlexW1598065184MaRDI QIDQ3644765

Hongseok Yang, Bernhard Reus, Lars Birkedal, Jan Schwinghammer

Publication date: 12 November 2009

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

Full work available at URL: https://arxiv.org/abs/1109.3031

Mathematics Subject Classification ID

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

Cites Work

• An observationally complete program logic for imperative higher-order functions
• Solving reflexive domain equations in a category of complete metric spaces
• Relational properties of domains
• Separation logic, abstraction and inheritance
• Domain-Theoretic Foundations of Functional Programming
• A Simple Model of Separation Logic for Higher-Order Store
• Separation Logic for Higher-Order Store
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• The Category-Theoretic Solution of Recursive Domain Equations
• The Logic of Bunched Implications
• Ynot
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages

Related Items (8)

Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Symbolic execution proofs for higher order store programs ⋮ Time Bounds for General Function Pointers ⋮ The category-theoretic solution of recursive metric-space equations ⋮ Specification patterns for reasoning about recursion through the store ⋮ Realisability semantics of parametric polymorphism, general references and recursive types ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq ⋮ Specification Patterns and Proofs for Recursion through the Store

Uses Software

• Ynot

This page was built for publication: Nested Hoare Triples and Frame Rules for Higher-Order Store