Formal certification of a compiler back-end or: programming a compiler with a proof assistant.

Xavier Leroy

Browse the full POPL paper archive.