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

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

CoqではOCamlのモジュールやファンクターみたいな機構があり、それらを使うとOCamlのモジュールと密接に連携することができる。
今回はOCamlのモジュールをCoqで使用する方法を紹介する。

  • Coqのソースファイル
    • ObjectiveCaml.v (OCamlから渡されるOCamlモジュールのシグネチャを記述)
    • Main.v (CoqのメインファイルでOCamlモジュールを受け取るファンクター。)
  • OCamlのソースファイル
    • oCaml.ml (CoqにわたすOCamlモジュール)
    • main.ml (単なるエントリポイント。ここは変わらない)

あとで書く