Pilsner: a compositionally verified compiler for a higher-order imperative language.

Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis

Browse the full ICFP paper archive.