A Kripke logical relation for effect-based program transformations

DOI10.1016/J.IC.2016.04.003zbMath1345.68095OpenAlexW2461817804MaRDI QIDQ2629855

Guilhem Jaber, Jacob Thamsborg, Lars Birkedal, Filip Sieczkowski

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

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

Related Items (1)

On the Versatility of Open Logical Relations

Uses Software

• Cyclone

Cites Work

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

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