A Kripke logical relation for effect-based program transformations

DOI10.1016/J.IC.2016.04.003MaRDI QIDQ2629855zbMATH OpenOpenAlexFDO

Authors Lars Birkedal, Guilhem Jaber, Filip Sieczkowski, Jacob Thamsborg

Publication date 7 July 2016

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2016.04.003

zbMATH Keywords

program transformationeffect type systemKripke logical relation

Mathematics Subject Classification ID

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

Recommendations

• A Kripke logical relation for effect-based program transformations
• A program transformation from equational programs into logic programs
• Transformations of logic programs
• Transformations of logic programs
• A Program Transformation for Tracing Functional Logic Computations
• A kripke-kleene semantics for logic programs*
• An Intensional Semantics for Elementary Program Transformations
• Logic Based Program Synthesis and Transformation
• Program transformations in a denotational setting
• scientific article; zbMATH DE number 2084335

Cites work

• A Kripke logical relation for effect-based program transformations
• A concurrent logical relation
• Fictional separation logic
• Logical relations for fine-grained concurrency
• On regions and linear types (extended abstract)
• Polymorphism and separation in Hoare type theory
• Programming Languages and Systems
• Reading, Writing and Relations
• Realisability semantics of parametric polymorphism, general references and recursive types
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Relational properties of domains
• Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages
• Solving reflexive domain equations in a category of complete metric spaces
• State-dependent representation independence
• Step-indexed Kripke models over recursive worlds
• The category-theoretic solution of recursive metric-space equations
• The impact of higher-order state and control effects on local relational reasoning
• Typing termination in a higher-order concurrent imperative language

Cited in

(6)

• A concurrent logical relation
• A fibrational tale of operational logical relations: pure, effectful and differential
• A Kripke logical relation between ML and assembly
• Abstract effects and proof-relevant logical relations
• A Kripke logical relation for effect-based program transformations
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem

Describes a project that uses

Uses Software

• Cyclone

This page was built for publication: A Kripke logical relation for effect-based program transformations

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