A verified compiler for a lazy functional language - View it on GitHub