某所にあった問題。（もし僕の答えが合っていたら）ネタバレ。追記もあります（←アンテナに反映させるため）。

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-b…