Coq2Scala

Coq to Scala

English

概要

Coq2ScalaCoqのExtraction機能に関する拡張です。 Coq2ScalaはCoqで定義されたアルゴリズムをScalaと連携しJVM上で高速に動作させることを可能にします。

アルゴリズム

Mprime_annot

ダウンロード

こちらからパッチをダウンロードできます:

https://bitbucket.org/yoshihiro503/coq2scala/downloads

インストール

  1. 上記から差分ファイルをダウンロードし、対応するcoqのソースコードもCoq本家から取得します。
  2. patchコマンドでパッチを適用します。
   $ cd coq-8.3pl2/
   $ patch -p 2 < ~/Downloads/coq2scala-1.0_for_coq-8.3pl2
  1. あとはcoqと同様
   $ ./configure -prefix ~/coq2scala
   $ make world
   $ make install

使い方

Extraction Language Scala. と指定し、あとは通常のCoqと同様。

coq2scalaを利用したソフトウェア

未実装機能

  • モジュール機能
  • CoInductive, CoFixpoint
  • Extract Inductiveコマンドによる指定