Paket: coq (8.1.pl3+dfsg-1 und andere)

[ Quellcode: coq  ]

Beweis-Assistent für Logik höherer Ordnung (Toplevel und Compiler)

Coq ist ein Beweis-Assistent für Logik höherer Ordnung, der die Entwicklung von Computerprogrammen, die konsistent mit ihrer formalen Spezifikation sind, erlaubt. Er wird mittels Objective Caml und Camlp4 entwickelt. Für weitere Informationen, siehe <http://coq.inria.fr/>.

Dieses Paket enthält coqtop, eine Befehlszeilen-Schnittstelle zu Coq.

Eine grafische Oberfläche für Coq ist in dem coqide-Paket. Coq kann auch mit ProofGeneral verwendet werden, was die Bearbeitung der Beweise mit Emacs und XEmacs ermöglicht. Dies erfordert die Installation des Pakets proofgeneral-coq.

Markierungen: Software-Entwicklung: Compiler, Feld: Mathematik, Implementiert in: OCaml, Benutzer-Schnittstellen: Kommandozeile, Text-basiert interaktiv, Rolle: Programm, Zweck: Hilfswerkzeug, GUI-Baukasten: Ncurses TUI

Andere Pakete mit Bezug zu coq

• dep: coq-libs (= 8.1.pl3+dfsg-1)

  proof assistant for higher-order logic (theories)

• dep: emacsen-common

  Gemeinsame Funktionen aller Emacs-Varianten

• dep: libc6 (>= 2.7-1) [nicht alpha, ia64]

  GNU C Library: Shared libraries
  auch ein virtuelles Paket, bereitgestellt durch libc6-udeb

• dep: libc6.1 (>= 2.7-1) [alpha, ia64]

  GNU C Library: Shared libraries
  auch ein virtuelles Paket, bereitgestellt durch libc6.1-udeb

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

  GCC Support-Bibliothek

• dep: libncurses5 (>= 5.6+20071006-3)

  gemeinsam benutzte Bibliotheken für Terminalsteuerung

• dep: ocaml-base-nox-3.10.2

  virtuelles Paket, bereitgestellt durch ocaml-base-nox

• dep: tex-common (>= 1.10)

  Gemeinsame Infrastruktur zum Erstellen und Installieren von TeX

• rec: coqide

  proof assistant for higher-order logic (gtk interface)

  oder proofgeneral-coq

  generic interface for proof assistants - coq support

• sug: cle

  Fügt jedem Kommandozeilen Programm 'readline' hinzu

• sug: coq-doc

  documentation for Coq in html format

• sug: ledit

  Zeileneditor für interaktive Programme

• 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 herunterladen

Download für alle verfügbaren Architekturen

Architektur	Version	Paketgröße	Größe (installiert)	Dateien
alpha	8.1.pl3+dfsg-1+b2	4.238,4 kB	19.404,0 kB	[Liste der Dateien]
amd64	8.1.pl3+dfsg-1+b2	8.825,9 kB	33.696,0 kB	[Liste der Dateien]
arm	8.1.pl3+dfsg-1+b2	4.091,6 kB	18.804,0 kB	[Liste der Dateien]
armel	8.1.pl3+dfsg-1+b2	4.116,3 kB	18.864,0 kB	[Liste der Dateien]
hppa	8.1.pl3+dfsg-1+b2	4.180,0 kB	18.988,0 kB	[Liste der Dateien]
i386	8.1.pl3+dfsg-1+b2	8.264,1 kB	30.272,0 kB	[Liste der Dateien]
ia64	8.1.pl3+dfsg-1+b2	4.370,6 kB	20.380,0 kB	[Liste der Dateien]
mips	8.1.pl3+dfsg-1+b2	4.145,0 kB	19.336,0 kB	[Liste der Dateien]
mipsel	8.1.pl3+dfsg-1+b2	4.132,1 kB	19.316,0 kB	[Liste der Dateien]
powerpc	8.1.pl3+dfsg-1+b2	9.236,7 kB	32.096,0 kB	[Liste der Dateien]
s390	8.1.pl3+dfsg-1+b2	4.226,0 kB	19.076,0 kB	[Liste der Dateien]
sparc	8.1.pl3+dfsg-1+b2	9.245,7 kB	32.372,0 kB	[Liste der Dateien]