Compcert C, also written in Coq, is another interesting C compiler: http://compcert.inria.fr/