[  sarge  ] [  etch  ] [  etch-m68k  ] [  lenny  ] [  sid  ] [  experimental  ]
[ ソース: coq  ]

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

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

Coq は、高位論理用の証明アシスタントであり、形式仕様の整合性を保つコン ピュータプログラムの開発が可能です。Objective Caml と Camlp4 を用いて 開発されています。詳細は、<http://coq.inria.fr/> を参照してください。

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

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

タグ: ソフトウェア開発: コンパイラ, 分野: 数学, 実装言語: OCaml, ユーザインタフェース: コマンドライン, テキストベースの対話, 役割: プログラム, 対象範囲: ユーティリティ, インタフェースツールキット: Ncurses TUI

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

  • 依存
  • 推奨
  • 提案
  • dep: coq-libs (= 8.1.pl3+dfsg-1)
    高位論理用の証明アシスタント (理論)
  • dep: emacsen-common
    全 Emacsen 用の共通機能
  • dep: hurd [hurd-i386]
    GNU Hurd
  • dep: libc0.1 (>= 2.7-1) [kfreebsd-amd64, kfreebsd-i386]
    GNU C ライブラリ: 共有ライブラリ
    以下のパッケージによって提供される仮想パッケージでもあります: libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    GNU C ライブラリ: 共有ライブラリ
    以下のパッケージによって提供される仮想パッケージでもあります: libc0.3-udeb
  • dep: libc6 (>= 2.5-5) [m68k]
    GNU C ライブラリ: 共有ライブラリ
    以下のパッケージによって提供される仮想パッケージでもあります: libc6-udeb
    dep: libc6 (>= 2.7-1) [alpha, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k 以外]
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    GNU C ライブラリ: 共有ライブラリ
    以下のパッケージによって提供される仮想パッケージでもあります: libc6.1-udeb
  • dep: libgcc1 (>= 1:4.3) [armel]
    GCC 共有ライブラリ
  • dep: libncurses5 (>= 5.6+20071006-3)
    ターミナル処理用共有ライブラリ
  • dep: ocaml-base-nox-3.10.2
    以下のパッケージによって提供される仮想パッケージです: ocaml-base-nox
  • dep: tex-common (>= 1.10) [hurd-i386 以外]
    common infrastructure for building and installing TeX
    dep: tex-common (>= 1.11) [hurd-i386]
  • rec: coqide
    高位論理用証明アシスタント (gtk インターフェイス)
    または proofgeneral-coq
    高位論理用証明アシスタント (gtk インターフェイス)
  • sug: cle
    コマンドライン駆動型ツールの readline 付ラッパー
  • sug: coq-doc
    documentation for Coq in html format
  • sug: ledit
    対話的プログラム向けのラインエディタ
  • sug: ocaml-nox (>= 3.08)
    ML language implementation with a class-based object system
  • sug: proofgeneral-coq
    generic interface for proof assistants - coq support

coq のダウンロード

すべての利用可能アーキテクチャ向けのダウンロード
アーキテクチャ バージョン パッケージサイズ インストールサイズ ファイル
alpha 8.1.pl3+dfsg-1+b2 4,238.4 kB19404 kB [ファイル一覧]
amd64 8.1.pl3+dfsg-1+b2 8,825.9 kB33696 kB [ファイル一覧]
arm 8.1.pl3+dfsg-1+b2 4,091.6 kB18804 kB [ファイル一覧]
armel 8.1.pl3+dfsg-1+b2 4,116.3 kB18864 kB [ファイル一覧]
hppa 8.1.pl3+dfsg-1+b2 4,180.0 kB18988 kB [ファイル一覧]
hurd-i386 8.1.pl3+dfsg-1 8,213.1 kB30412 kB [ファイル一覧]
i386 8.1.pl3+dfsg-1+b2 8,264.1 kB30272 kB [ファイル一覧]
ia64 8.1.pl3+dfsg-1+b2 4,370.6 kB20380 kB [ファイル一覧]
kfreebsd-amd64 (非公式の移植版) 8.1.pl3+dfsg-1+b2 4,166.9 kB19216 kB [ファイル一覧]
kfreebsd-i386 (非公式の移植版) 8.1.pl3+dfsg-1+b2 8,258.0 kB30720 kB [ファイル一覧]
m68k 8.1.pl3+dfsg-1+b2 4,014.9 kB18580 kB [ファイル一覧]
mips 8.1.pl3+dfsg-1+b2 4,145.0 kB19336 kB [ファイル一覧]
mipsel 8.1.pl3+dfsg-1+b2 4,132.1 kB19316 kB [ファイル一覧]
powerpc 8.1.pl3+dfsg-1+b2 9,236.7 kB32096 kB [ファイル一覧]
s390 8.1.pl3+dfsg-1+b2 4,226.0 kB19076 kB [ファイル一覧]
sparc 8.1.pl3+dfsg-1+b2 9,245.7 kB32372 kB [ファイル一覧]