Aarhus University Seal / Aarhus Universitets segl

A relational realizability model for higher-order stateful

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Standard

A relational realizability model for higher-order stateful. / Birkedal, Lars; Støvring, Kristian; Thamsborg, Jacob.

In: Journal of Logic and Algebraic Programming, Vol. 81, No. 4, 2012, p. 491-521.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Harvard

APA

CBE

Birkedal L, Støvring K, Thamsborg J. 2012. A relational realizability model for higher-order stateful. Journal of Logic and Algebraic Programming. 81(4):491-521.

MLA

Birkedal, Lars, Kristian Støvring and Jacob Thamsborg. "A relational realizability model for higher-order stateful". Journal of Logic and Algebraic Programming. 2012, 81(4). 491-521.

Vancouver

Birkedal L, Støvring K, Thamsborg J. A relational realizability model for higher-order stateful. Journal of Logic and Algebraic Programming. 2012;81(4):491-521.

Author

Birkedal, Lars ; Støvring, Kristian ; Thamsborg, Jacob. / A relational realizability model for higher-order stateful. In: Journal of Logic and Algebraic Programming. 2012 ; Vol. 81, No. 4. pp. 491-521.

Bibtex

@article{6ca49a48c9bf4c7cb1266d191624a2e2,
title = "A relational realizability model for higher-order stateful",
abstract = "We present a realizability model for reasoning about contextual equivalence of higher-order programs with impredicative polymorphism, recursive types, and higher-order mutable state.The model combines the virtues of two recent earlier models: (1) Ahmed, Dreyer, and Rossberg{\textquoteright}s step-indexed logical relations model, which was designed to facilitate proofs of representation independence for “state-dependent” ADTs and (2) Birkedal, St{\o}vring, and Thamsborg{\textquoteright}s realizability logical relations model, which was designed to facilitate abstract proofs without tedious step-index arithmetic. The resulting model can be used to give abstract proofs of representation independence for “state-dependent” ADTs.",
author = "Lars Birkedal and Kristian St{\o}vring and Jacob Thamsborg",
year = "2012",
language = "English",
volume = "81",
pages = "491--521",
journal = "Journal of Logic and Algebraic Programming",
issn = "2352-2208",
publisher = "Elsevier",
number = "4",

}

RIS

TY - JOUR

T1 - A relational realizability model for higher-order stateful

AU - Birkedal, Lars

AU - Støvring, Kristian

AU - Thamsborg, Jacob

PY - 2012

Y1 - 2012

N2 - We present a realizability model for reasoning about contextual equivalence of higher-order programs with impredicative polymorphism, recursive types, and higher-order mutable state.The model combines the virtues of two recent earlier models: (1) Ahmed, Dreyer, and Rossberg’s step-indexed logical relations model, which was designed to facilitate proofs of representation independence for “state-dependent” ADTs and (2) Birkedal, Støvring, and Thamsborg’s realizability logical relations model, which was designed to facilitate abstract proofs without tedious step-index arithmetic. The resulting model can be used to give abstract proofs of representation independence for “state-dependent” ADTs.

AB - We present a realizability model for reasoning about contextual equivalence of higher-order programs with impredicative polymorphism, recursive types, and higher-order mutable state.The model combines the virtues of two recent earlier models: (1) Ahmed, Dreyer, and Rossberg’s step-indexed logical relations model, which was designed to facilitate proofs of representation independence for “state-dependent” ADTs and (2) Birkedal, Støvring, and Thamsborg’s realizability logical relations model, which was designed to facilitate abstract proofs without tedious step-index arithmetic. The resulting model can be used to give abstract proofs of representation independence for “state-dependent” ADTs.

M3 - Journal article

VL - 81

SP - 491

EP - 521

JO - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

SN - 2352-2208

IS - 4

ER -