関数型言語マニアのための論文紹介６：定理証明器で書かれたCコンパイラ - sumiiのブログFormal certification of a compiler back-end, or: programming a compiler with a proof assistant. Xavier Leroy. POPL 2006. http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf ソースコードとか。 http://pauillac.inria.fr/~xleroy/compcert-backend/ 著者のXavier LeroyはOCamlの作者です。 （ネイティブコードを吐く）コンパイラを作ったことがある人なら、ごく稀にしか起きない、わけのわからないバグに悩まされたことがきっとあると思います。そういうバグがあると、コンパイラを作る人どころか、それを使うプログラマも悩まされます。これはMLのような型つき言語でコ
