Fri 12 Jan 2018 15:50 - 16:15 at Watercourt - Types for State Chair(s): Neel Krishnaswami

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 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

15:50 - 17:05: Research Papers - Types for State at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
POPL-2018-papers15:50 - 16:15
Amin Timanyimec-Distrinet KU-Leuven, Leo StefanescoENS Lyon, Morten Krogh-JespersenAarhus University, Lars BirkedalAarhus University
POPL-2018-papers16:15 - 16:40
Danel AhmanInria Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris and ENS Paris, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
POPL-2018-papers16:40 - 17:05
Ralf JungMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology, Derek DreyerMPI-SWS