Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
From MaRDI portal
Publication:5310672
DOI10.2168/LMCS-2(5:1)2006zbMath1127.68019MaRDI QIDQ5310672
Hongseok Yang, Noah Torp-Smith, Lars Birkedal
Publication date: 11 October 2007
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Crowfoot: A Verifier for Higher-Order Store Programs, Symbolic execution proofs for higher order store programs, A Kripke logical relation for effect-based program transformations, Towards imperative modules: reasoning about invariants and sharing of mutable state, On assertion-based encapsulation for object invariants and simulations, Specification patterns for reasoning about recursion through the store, Step-Indexed Kripke Model of Separation Logic for Storable Locks, Relational Decomposition, Specification Patterns and Proofs for Recursion through the Store, Nested Hoare Triples and Frame Rules for Higher-Order Store
