Lambda the Ultimate

Xavier Leroy's contribution to POPL'06 is Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, which describes a fairly realistic mini-compiler from a subset of C, called Cminor, to PPC assembler.

So what? It's written entirely in Coq, which pretty much makes a certified compiler for free, and all done in a particularly easy way to leverage if you want to show particular implementations correct.

He's got a resource page up with the implementation (which he calls CompCert), and some further notes.