A semantic foundation for hidden state

DOI10.1007/978-3-642-12032-9_2MaRDI QIDQ3557840zbMATH OpenOpenAlexFDO

Authors Hongseok Yang, François Pottier, Bernhard Reus, Jan Schwinghammer, Lars Birkedal

Publication date 27 April 2010

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-12032-9_2

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A step-indexed Kripke model of hidden state
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces
• Separation and information hiding
• Dynamic boundaries: information hiding by second order framing with first order assertions

Cited in

(7)

• Symbolic execution proofs for higher order store programs
• Crowfoot: A Verifier for Higher-Order Store Programs
• A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces
• Realisability semantics of parametric polymorphism, general references and recursive types
• Specification patterns for reasoning about recursion through the store
• A step-indexed Kripke model of hidden state
• Syntactic soundness proof of a type-and-capability system with hidden state

This page was built for publication: A semantic foundation for hidden state

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