#Coq to Scala

[English](/en/Coq2Scala)

##概要
[Coq2Scala]()は[Coq](http://coq.inria.fr/)のExtraction機能に関する拡張です。
Coq2ScalaはCoqで定義されたアルゴリズムを[Scala](http://scala-lang.org/)と連携しJVM上で高速に動作させることを可能にします。

- 開発者: 今井宜洋([ITプランニング](http://www.itpl.co.jp/))、姜帆([東京大学 情報理工学系研究科](http://www.i.u-tokyo.ac.jp/))
- ハッシュタグ: [#coq2scala](https://twitter.com/#!/search/realtime/%23coq2scala)
- リポジトリ: [http://bitbucket.org/yoshihiro503/coq2scala](http://bitbucket.org/yoshihiro503/coq2scala)

##アルゴリズム
[Mprime_annot]()

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

[https://bitbucket.org/yoshihiro503/coq2scala/downloads](https://bitbucket.org/yoshihiro503/coq2scala/downloads)

##インストール
1. 上記から差分ファイルをダウンロードし、対応するcoqのソースコードも[Coq本家](http://coq.inria.fr/distrib/)から取得します。
2. patchコマンドでパッチを適用します。

~~~ { .sh }
   $ cd coq-8.4/
   $ patch -p1 < ~/Downloads/coq2scala-0.1_for_coq-8.4
~~~

3. あとはcoqと同様

~~~ { .sh }
   $ ./configure -prefix ~/coq2scala
   $ make world
   $ make install
~~~

##使い方

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

##coq2scalaを利用したソフトウェア
- [CoqInCoq for Scala](https://bitbucket.org/yoshihiro503/coqincoq_scala/): [解説](http://d.hatena.ne.jp/yoshihiro503/20111207#p1)

##未実装機能

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