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

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

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)

Cited In (3)

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

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)