CompCert
正当性を証明された
C
Compiler
Coq
で証明された
プロジェクトリーダーは
Xavier Leroy
INRIA
website
github
parserはOCaml実装
コンパイラの正当性とは
入力言語と、出力言語の各意味を数式で表現することで、
任意の入力に対して、出力が同じものを表すことを示すことができる
最適化する前と後で動作が変わらないことを保証
関連
VeriFast
https://github.com/verifast/verifast
https://people.cs.kuleuven.be/~bart.jacobs/verifast/
Frama-C
https://frama-c.com/
https://en.wikipedia.org/wiki/Frama-C
https://www.slideshare.net/mzpi/20110514-boost3
Program Logics for Certified Compilers
という本
CompCertの人たちが書いている
Coq
で
Separation logic
するなどが書かれているらしい
http://compcert.inria.fr/doc/
http://gallium.inria.fr/~scherer/gagallium/register-allocation/index.html