Step-indexed kripke models over recursive worlds

DOI10.1145/1926385.1926401zbMath1284.68102OpenAlexW4235454363MaRDI QIDQ5408537

Hongseok Yang, Bernhard Reus, Kristian Støvring, Jacob Thamsborg, Lars Birkedal, Jan Schwinghammer

Publication date: 10 April 2014

Published in: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:f2d38299-0326-4633-b77e-6f5d3e7ee2ac

zbMATH Keywords

Kripke modelsultrametric spacesstep-indexed modelsindirection theorycapability calculusframe rules

Mathematics Subject Classification ID

Metric spaces, metrizability (54E35) Theory of programming languages (68N15) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (11)

Symbolic execution proofs for higher order store programs ⋮ A Kripke logical relation for effect-based program transformations ⋮ Bringing Order to the Separation Logic Jungle ⋮ Time Bounds for General Function Pointers ⋮ Specification patterns for reasoning about recursion through the store ⋮ Verified Software Toolchain ⋮ Step-Indexed Kripke Model of Separation Logic for Storable Locks ⋮ Transfinite Step-Indexing: Decoupling Concrete and Logical Steps ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq ⋮ Guarded cubical type theory ⋮ StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

Uses Software

• Mechanized Semantic Library

This page was built for publication: Step-indexed kripke models over recursive worlds