Revision cb3a4c83ceb6ce749420b7a08a365c8ad04ab896

Coq2Scala

Coq to Scala

概要

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

ダウンロード

こちらからダウンロードできます:

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

使い方

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

coq2scalaを利用したソフトウェア

未実装機能

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