#Coq to Scala

[日本語](/Coq2Scala)

##Abstract

[Coq2Scala]() is an extention to [Coq](http://coq.inria.fr/) Extraction.
Coq will be able to generate Scala code from proved algorithms.

- author: Yoshihiro Imai([IT Planning Inc](http://www.itpl.co.jp/)), Jiang Fan([The University of Tokyo](http://www.i.u-tokyo.ac.jp/))
- hashtag: [#coq2scala](https://twitter.com/#!/search/realtime/%23coq2scala)
- sources: [http://bitbucket.org/yoshihiro503/coq2scala](http://bitbucket.org/yoshihiro503/coq2scala)

##Algorithm
[Mprime_annot]()

##Download
The extension is provided as a patch for Coq source code:

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

##Install
1. Download the patch file and corresponding version of Coq source code from [CoqDistributes](http://coq.inria.fr/distrib/).
2. Apply the patch.

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

3. Make and Install

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

##How to Use
The vernacular command : "Extraction Language Scala." will be available.

##Examples
- [CoqInCoq for Scala](https://bitbucket.org/yoshihiro503/coqincoq_scala/): [article](http://d.hatena.ne.jp/yoshihiro503/20111207#p1)

##Unsupported Features

- Modules
- CoInductive, CoFixpoint
- Extract Inductive command