A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
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 langauge with monadic encapsulation of state. We have formalized all the technical development and results in Coq.
Fri 12 JanDisplayed time zone: Tijuana, Baja California change
15:50 - 17:05
|A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST|
|Recalling a Witness: Foundations and Applications of Monotonic State|
Danel Ahman Inria Paris, Cédric Fournet Microsoft Research, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris and ENS Paris, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft ResearchPre-print
|RustBelt: Securing the Foundations of the Rust Programming Language|