A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces

DOI10.1007/978-3-642-19805-2_21zbMATH Open1326.68105OpenAlexW1608782706MaRDI QIDQ3000617FDOQ3000617

Authors Kristian Støvring, Jan Schwinghammer, Lars Birkedal

Publication date 19 May 2011

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-19805-2_21

Mathematics Subject Classification ID

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

Recommendations

• A step-indexed Kripke model of hidden state
• Nested Hoare triples and frame rules for higher-order store
• A semantic foundation for hidden state
• Step-indexed Kripke models over recursive worlds
• Syntactic soundness proof of a type-and-capability system with hidden state

Cited in

(3)

• A semantic foundation for hidden state
• A step-indexed Kripke model of hidden state
• Step-indexed Kripke models over recursive worlds

This page was built for publication: A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces

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