2009-01-22 CoqでOCamlのモジュールを使う CoqではExtractionという機能があるためにOCamlやHaskellなどの関数型言語との連携が容易である。 CoqでOCamlの型や関数を使いたい場合は単に関数の引数として渡せば良いだけだからである。 ただ、沢山の型や関数を一度に渡したい場合、結構面倒である。CoqではOCamlのモジュールやファンクターみたいな機構があり、それらを使うとOCamlのモジュールと密接に連携することができる。 今回はOCamlのモジュールをCoqで使用する方法を紹介する。 Coqのソースファイル ObjectiveCaml.v (OCamlから渡されるOCamlモジュールのシグネチャを記述) Main.v (CoqのメインファイルでOCamlモジュールを受け取るファンクター。) OCamlのソースファイル oCaml.ml (CoqにわたすOCamlモジュール) main.ml (単なるエントリポイント。ここは変わらない) 続きを読む