読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

OCamlerのためのCoq便利モジュールを公開してみた

Coq OCaml Extraction


このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。

ダウンロード: http://sourceforge.jp/projects/coqbase/

具体的には以下のことを定義した。

  • 標準出力へ出力するprint, println関数
  • 命令をつなげるセミコロン演算子
  • 依存型を使った型安全なprintf関数
  • natからOCamlのint、stringからOCamlのstringへの相互変換関数
  • Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携