Transfinite Step-Indexing: Decoupling Concrete and Logical Steps

DOI10.1007/978-3-662-49498-1_28zbMath1335.68071OpenAlexW2502922259MaRDI QIDQ2802498

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) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

A Higher-Order Logic for Concurrent Termination-Preserving Refinement ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item

Uses Software

• Toolchain

Cites Work

• Unnamed Item
• Unnamed Item
• The category-theoretic solution of recursive metric-space equations
• Iris
• Step-Indexed Relational Reasoning for Countable Nondeterminism
• Logical relations for fine-grained concurrency
• Biorthogonality, step-indexing and compiler correctness
• The impact of higher-order state and control effects on local relational reasoning
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• A very modal model of a modern, major, general type system
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• A theory of indirection via approximation
• State-dependent representation independence
• Step-indexed kripke models over recursive worlds
• A kripke logical relation between ML and assembly
• Impredicative Concurrent Abstract Predicates
• Program Logics for Certified Compilers
• Programming Languages and Systems

This page was built for publication: Transfinite Step-Indexing: Decoupling Concrete and Logical Steps