A relational realizability model for higher-order stateful

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

  • Lars Birkedal
  • Kristian Støvring, IT University of Copenhagen, Denmark
  • Jacob Thamsborg, IT University of Copenhagen, Denmark
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.
Original languageEnglish
JournalJournal of Logic and Algebraic Programming
Volume81
Issue4
Pages (from-to)491-521
Number of pages31
ISSN2352-2208
Publication statusPublished - 2012
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 78994214