Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis. Pilsner: a compositionally verified compiler for a higher-order imperative language. In Kathleen Fisher, John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. pages 166-178, ACM, 2015. [doi]
Abstract is missing.