Step-indexed Kripke models over recursive worlds

DOI10.1145/1926385.1926401MaRDI QIDQ5408537zbMATH OpenOpenAlexFDO

Authors Bernhard Reus, Kristian Støvring, Jacob Thamsborg, Hongseok Yang, 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

capability calculusframe rulesindirection theoryKripke modelsstep-indexed modelsultrametric spaces

Mathematics Subject Classification ID

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

Recommendations

• Transfinite step-indexing: decoupling concrete and logical steps
• Step-indexed Kripke model of separation logic for storable locks
• A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Step-indexed relational reasoning for countable nondeterminism

Cited in

(14)

• Guarded cubical type theory
• A Kripke logical relation for effect-based program transformations
• Transfinite step-indexing: decoupling concrete and logical steps
• Symbolic execution proofs for higher order store programs
• Verified software toolchain (invited talk)
• A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces
• Verifying object-oriented programs with higher-order separation logic in Coq
• Time bounds for general function pointers
• Specification patterns for reasoning about recursion through the store
• StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
• Bringing Order to the Separation Logic Jungle
• Step-indexed Kripke model of separation logic for storable locks
• Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle
• A logical approach to type soundness

Describes a project that uses

Uses Software

• Mechanized Semantic Library

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

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