Pure

A verified compiler for a lazy functional language