Joachim Breitner: Formally proving a compiler transformation safe. Haskell 2015: 35-46