Transfinite step-indexing: decoupling concrete and logical steps
DOI10.1007/978-3-662-49498-1_28zbMATH Open1335.68071OpenAlexW2502922259MaRDI QIDQ2802498FDOQ2802498
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
Recommendations
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cites Work
- State-dependent representation independence
- Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
- Impredicative concurrent abstract predicates
- Step-indexed Kripke models over recursive worlds
- A very modal model of a modern, major, general type system
- Programming Languages and Systems
- The category-theoretic solution of recursive metric-space equations
- Logical relations for fine-grained concurrency
- Biorthogonality, step-indexing and compiler correctness
- A Kripke logical relation between ML and assembly
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Program logics for certified compilers
- A theory of indirection via approximation
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Title not available (Why is that?)
- The impact of higher-order state and control effects on local relational reasoning
- A concurrent logical relation
- Step-indexed relational reasoning for countable nondeterminism
Cited In (6)
Uses Software
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)
