パッケージ: coq (8.3.pl3+dfsg-1~bpo60+1) [backports]

[ ソース: coq  ]

高階述語論理証明アシスタント (トップレベルおよびコンパイラ)

Coq は、高階述語論理用の証明アシスタントであり、形式的な仕様との整合性を保 つコンピュータプログラムの開発が可能です。Objective Caml と Camlp5 を用いて 開発されています。

本パッケージは Coq へのコマンドラインインターフェイス coqtop を提供します。

Coq 用 GUI は coqide パッケージにて提供されます。 Coq は ProofGeneral とも併用でき、証明を emacs や xemacs により編集できるよ うになります。これには proofgeneral-coq パッケージのインストールが必要です。

その他の coq 関連パッケージ

• dep: coq-theories (= 8.3.pl3+dfsg-1~bpo60+1)

  高階論理用の証明アシスタント (理論)

• dep: emacsen-common

  全 Emacsen 用の共通機能

• dep: libc0.1 (>= 2.7) [kfreebsd-amd64, kfreebsd-i386]

  組込用 GNU C ライブラリ: 共有ライブラリ
  以下のパッケージによって提供される仮想パッケージでもあります: libc0.1-udeb

• dep: libc6 (>= 2.7) [amd64, i386, powerpc]

  組込用 GNU C ライブラリ: 共有ライブラリ
  以下のパッケージによって提供される仮想パッケージでもあります: libc6-udeb

• dep: libcoq-ocaml-2n499 [i386, kfreebsd-i386, powerpc]

  以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml

• dep: libcoq-ocaml-3ldl2 [amd64, kfreebsd-amd64]

  以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml

• dep: libcoq-ocaml-cg3k8 [armel, ia64, mips, mipsel, s390]

  以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml

• dep: ocaml-base-nox-3.11.2

  パッケージは利用できません

• rec: coqide

  高階論理用証明アシスタント (gtk インターフェイス)

  または proofgeneral-coq

  証明アシスタント用の汎用インターフェイス - coq サポート

• sug: coq-doc

  documentation for Coq

• sug: ledit

  対話的プログラム向けのラインエディタ

  または readline-editor

  パッケージは利用できません

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: ocaml-nox

  クラスベースのオブジェクトシステムを持った ML 言語の実装

• sug: proofgeneral-coq

  証明アシスタント用の汎用インターフェイス - coq サポート

• sug: why (>= 2.19)

  A software verification tool

coq のダウンロード

すべての利用可能アーキテクチャ向けのダウンロード

アーキテクチャ	パッケージサイズ	インストールサイズ	ファイル
amd64	5,467.9 kB	18,280.0 kB	[ファイル一覧]
armel	1,736.1 kB	8,224.0 kB	[ファイル一覧]
i386	4,768.9 kB	14,732.0 kB	[ファイル一覧]
ia64	1,735.6 kB	8,224.0 kB	[ファイル一覧]
kfreebsd-amd64	5,461.6 kB	18,422.0 kB	[ファイル一覧]
kfreebsd-i386	4,766.3 kB	14,788.0 kB	[ファイル一覧]
mips	1,735.5 kB	8,224.0 kB	[ファイル一覧]
mipsel	1,734.0 kB	8,224.0 kB	[ファイル一覧]
powerpc	5,354.2 kB	15,832.0 kB	[ファイル一覧]
s390	1,732.5 kB	8,224.0 kB	[ファイル一覧]