パッケージ: coq (8.3.pl4+dfsg-1 など)

[ ソース: coq  ]

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

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

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

Coq のグラフィカルインターフェースは coqide パッケージが提供します。 Coq は ProofGeneral とも併用でき、証明を emacs や xemacs で編集できるように なります。これには proofgeneral パッケージのインストールが必要です。

タグ: ソフトウェア開発: コンパイラ, 分野: 数学, 実装言語: implemented-in::ocaml, interface::commandline, ユーザインタフェース: テキストベースの対話, 役割: role::program, scope::utility, インタフェースツールキット: Ncurses TUI

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

• dep: coq-theories (= 8.3.pl4+dfsg-1)

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

• dep: emacsen-common

  全 Emacsen 用の共通機能

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

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

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

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

• dep: libcoq-ocaml-ehg05 [armel]

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

• dep: libcoq-ocaml-m0xl3 [amd64, kfreebsd-amd64]

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

• dep: libcoq-ocaml-nc3h8 [armhf, ia64, mips, mipsel, s390, s390x]

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

• dep: libcoq-ocaml-s00f5 [i386, kfreebsd-i386, powerpc, sparc]

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

• dep: libgcc1 (>= 1:4.4.0) [armel]

  GCC 共有ライブラリ

• dep: ocaml-base-nox-3.12.1

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

• rec: coqide

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

  または proofgeneral

  generic frontend for proof assistants

• sug: coq-doc

  documentation for Coq

• sug: ledit

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

  または readline-editor

  以下のパッケージによって提供される仮想パッケージです: ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: ocaml-nox

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

• sug: proofgeneral

  generic frontend for proof assistants

• sug: why (>= 2.19)

  Software verification tool

coq のダウンロード

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

アーキテクチャ	バージョン	パッケージサイズ	インストールサイズ	ファイル
amd64	8.3.pl4+dfsg-1	5,542.9 kB	18,432.0 kB	[ファイル一覧]
armel	8.3.pl4+dfsg-1	5,967.2 kB	17,898.0 kB	[ファイル一覧]
armhf	8.3.pl4+dfsg-1	1,770.7 kB	8,225.0 kB	[ファイル一覧]
i386	8.3.pl4+dfsg-1	4,946.3 kB	15,045.0 kB	[ファイル一覧]
ia64	8.3.pl4+dfsg-1+b1	1,770.0 kB	8,225.0 kB	[ファイル一覧]
kfreebsd-amd64	8.3.pl4+dfsg-1	5,537.4 kB	18,311.0 kB	[ファイル一覧]
kfreebsd-i386	8.3.pl4+dfsg-1	4,940.5 kB	14,925.0 kB	[ファイル一覧]
mips	8.3.pl4+dfsg-1	1,768.9 kB	8,225.0 kB	[ファイル一覧]
mipsel	8.3.pl4+dfsg-1+b1	1,768.6 kB	8,225.0 kB	[ファイル一覧]
powerpc	8.3.pl4+dfsg-1	5,427.1 kB	15,876.0 kB	[ファイル一覧]
s390	8.3.pl4+dfsg-1	1,770.0 kB	8,225.0 kB	[ファイル一覧]
s390x	8.3.pl4+dfsg-1	1,771.4 kB	8,225.0 kB	[ファイル一覧]
sparc	8.3.pl4+dfsg-1	5,289.9 kB	15,807.0 kB	[ファイル一覧]