A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST

Amin Timany, Léo Stefanesco, Morten Krogh-Jeslpersen, and Lars Birkedal: A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. In PACMPL 2(POPL): 64:1-64:28 (2018), January 2018. https://doi.org/10.1145/3158152
.pdf Coq Development talk on youtube
Journal Paper
Keywords: ST Monad, Logical Relations, Functional Programming Languages, Theory of Programming Languages, Program Logics, Iris
Abstract.

We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.

The bibtex source for this publication:
@article{DBLP:journals/pacmpl/TimanySKB18,
  author    = {Amin Timany and
               L{\'{e}}o Stefanesco and
               Morten Krogh{-}Jespersen and
               Lars Birkedal},
  title     = {A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST},
  journal   = {{PACMPL}},
  volume    = {2},
  number    = {{POPL}},
  pages     = {64:1--64:28},
  year      = {2018},
  url       = {http://doi.acm.org/10.1145/3158152},
  doi       = {10.1145/3158152},
  timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/pacmpl/TimanySKB18},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}