Abstract

Coq2Scala is an extention to Coq Extraction. Coq will be able to generate Scala code from Coq definitions.

• author: Yoshihiro Imai(IT Planning Inc), Jiang Fan(The University of Tokyo)
• hashtag: #coq2scala
• sources: http://bitbucket.org/yoshihiro503/coq2scala

Download

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

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

Install

1. Download the patch file and corresponding version of Coq source code from CoqDistributes.
2. Apply the patch.

   $ cd coq-8.3pl2/
   $ patch -p 2 < ~/Downloads/coq2scala-1.0_for_coq-8.3pl2

3. Make and Install

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

How to Use

The vernacular command : “Extraction Language Scala.” will be available.

Examples

• CoqInCoq for Scala: article

Unsupported Features

• Modules
• CoInductive, CoFixpoint
• Extract Inductive command