Transfinite step-indexing: decoupling concrete and logical steps

DOI10.1007/978-3-662-49498-1_28MaRDI QIDQ2802498zbMATH OpenOpenAlexFDO

Authors Kasper Svendsen, Filip Sieczkowski, Lars Birkedal

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01408649/file/biglater-conf%20%281%29.pdf

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Programming Languages and Systems
• Step-indexed logical relations for probability
• Step-indexed Kripke models over recursive worlds
• Step-indexed relational reasoning for countable nondeterminism
• Step-indexed relational reasoning for countable nondeterminism

Cites work

• scientific article; zbMATH DE number 2003155 (Why is no real title available?)
• A Kripke logical relation between ML and assembly
• A concurrent logical relation
• A theory of indirection via approximation
• A very modal model of a modern, major, general type system
• Biorthogonality, step-indexing and compiler correctness
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Impredicative concurrent abstract predicates
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Logical relations for fine-grained concurrency
• Program logics for certified compilers
• Programming Languages and Systems
• State-dependent representation independence
• Step-indexed Kripke models over recursive worlds
• Step-indexed relational reasoning for countable nondeterminism
• The category-theoretic solution of recursive metric-space equations
• The impact of higher-order state and control effects on local relational reasoning
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency

Cited in

(6)

• Programming Languages and Systems
• Step-indexed logical relations for probability
• Coinduction in Flow: The Later Modality in Fibrations
• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• Step-indexed Kripke models over recursive worlds
• A higher-order logic for concurrent termination-preserving refinement

Describes a project that uses

Uses Software

• Toolchain

This page was built for publication: Transfinite step-indexing: decoupling concrete and logical steps

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