2009-01-22から1日間の記事一覧

CoqでOCamlのモジュールを使う

CoqではExtractionという機能があるためにOCamlやHaskellなどの関数型言語との連携が容易である。 CoqでOCamlの型や関数を使いたい場合は単に関数の引数として渡せば良いだけだからである。 ただ、沢山の型や関数を一度に渡したい場合、結構面倒である。Coq…