Package: coq (8.3.pl4+dfsg-2)

[ Source: coq  ]

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

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

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

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

Tags: Software Development: Compiler, Field: Mathematics, Implemented in: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Interface Toolkit: Ncurses TUI

Other Packages Related to coq

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

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

• dep: emacsen-common

  全 Emacsen 用の共通機能

• dep: libc6 (>= 2.7)

  組込用 GNU C ライブラリ: 共有ライブラリ
  also a virtual package provided by libc6-udeb

• dep: libcoq-ocaml-9fp12

  virtual package provided by libcoq-ocaml

• dep: ocaml-base-nox-3.12.1

  virtual package provided by ocaml-base-nox

• rec: coqide

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

  or proofgeneral

  generic frontend for proof assistants

• sug: coq-doc

  documentation for Coq

• sug: ledit

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

  or readline-editor

  virtual package provided by 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

Download coq

Download for all available architectures

Architecture	Package Size	Installed Size	Files
powerpc	5,431.2 kB	15,895.0 kB	[list of files]