Coq2Scala

#Coq to Scala

English

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

• 開発者: 今井宜洋(ITプランニング)、姜帆(東京大学 情報理工学系研究科)
• ハッシュタグ: #coq2scala
• リポジトリ: http://bitbucket.org/yoshihiro503/coq2scala

##アルゴリズム 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

3. あとはcoqと同様

   $ ./configure -prefix ~/coq2scala
   $ make world
   $ make install

##使い方

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

##coq2scalaを利用したソフトウェア - CoqInCoq for Scala: 解説

##未実装機能

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