Towards a verifiably correct compiler of expressions. Loosely based on a paper by Graham Hutton: Compiling Exceptions Correctly
A certified compiler of exceptions from my thesis (Agda)