2014-09-13から1日間の記事一覧

CoqからSMLへ

Coq OCaml SML

CoqにはExtractionという機能があり、Coqで書かれたソースコードから対応する他の言語のソースコードを出力する事ができます。今回はそのExtractionをStandard MLに対応させた事について書こうと思います。