Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 23-minute conference presentation from POPL 2018 that delves into the development of a logical relations model for analyzing higher-order functional programming languages with impredicative polymorphism, recursive types, and Haskell-style ST monad type with runST. Learn how researchers from KU Leuven, IRIF, CNRS, University of Paris Diderot, and Aarhus University demonstrate that runST effectively encapsulates state by proving heap independence of effectful computations. Discover how contextual refinements and equivalences for pure computations maintain their validity when runST is present - marking the first proven relational results for state monadic encapsulation in programming languages. Examine the complete technical development and results, which have been formally verified using Coq theorem prover.
