正当性を証明されたCCompiler

Coqで証明された

プロジェクトリーダーはXavier Leroy

parserはOCaml実装

コンパイラの正当性とは

入力言語と、出力言語の各意味を数式で表現することで、

任意の入力に対して、出力が同じものを表すことを示すことができる

最適化する前と後で動作が変わらないことを保証

関連

Program Logics for Certified Compilersという本

CompCertの人たちが書いている

CoqでSeparation logicするなどが書かれているらしい