en/Coq2Scala

Coq to Scala

日本語

Abstract

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

Algorithm

Mprime_annot

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.4/
   $ patch -p1 < ~/Downloads/coq2scala-0.1_for_coq-8.4
  1. Make and Install
   $ ./configure -prefix ~/coq2scala
   $ make world
   $ make install

How to Use

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

Examples

Unsupported Features

  • Modules
  • CoInductive, CoFixpoint
  • Extract Inductive command