ziman/excomp

A certified compiler of exceptions from my thesis (Agda)

Towards a verifiably correct compiler of expressions.
Loosely based on a paper by Graham Hutton: Compiling Exceptions Correctly