Paket: coq (8.2.pl2+dfsg-1)

[ Quellcode: coq  ]

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

Coq ist ein Beweis-Assistent für Logik höherer Ordnung. Er ermöglicht die Entwicklung von Computerprogrammen, die konsistent mit ihrer formalen Spezifikation sind. Er wird mittels Objective Caml und Camlp5 entwickelt.

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

Eine grafische Oberfläche für Coq ist in dem coqide-Paket enthalten. 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-theories (= 8.2.pl2+dfsg-1)

  proof assistant for higher-order logic (theories)

• dep: emacsen-common

  Gemeinsame Funktionen aller Emacs-Varianten

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

  Die »Embedded GNU C Library«: Laufzeitbibliotheken
  auch ein virtuelles Paket, bereitgestellt durch libc0.1-udeb

• dep: libc6 (>= 2.1.3) [s390]

  Die »Embedded GNU C Library«: Laufzeitbibliotheken
  auch ein virtuelles Paket, bereitgestellt durch libc6-udeb

  dep: libc6 (>= 2.2) [mips, mipsel]

  dep: libc6 (>= 2.4) [armel]

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

• dep: libc6.1 (>= 2.2) [ia64]

  Die »Embedded GNU C Library«: Laufzeitbibliotheken
  auch ein virtuelles Paket, bereitgestellt durch libc6.1-udeb

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

  GCC Support-Bibliothek

• dep: ocaml-base-nox-3.11.2

  virtuelles Paket, bereitgestellt durch ocaml-base-nox

• rec: coqide

  Beweis-Assistent für Logik höherer Ordnung (Gtk-Schnittstelle)

  oder proofgeneral-coq

  generic interface for proof assistants - coq support

• sug: coq-doc

  documentation for Coq

• sug: ledit

  Zeileneditor für interaktive Programme

  oder readline-editor

  virtuelles Paket, bereitgestellt durch ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: ocaml-nox

  ML-Implementierung mit einem klassenbasierten Objektsystem (ohne X)

• sug: proofgeneral-coq

  generic interface for proof assistants - coq support

• sug: why (>= 2.19)

  Ein Software-Verifizierungswerkzeug

coq herunterladen

Download für alle verfügbaren Architekturen

Architektur	Paketgröße	Größe (installiert)	Dateien
amd64	14.995,1 kB	52.460,0 kB	[Liste der Dateien]
armel	3.586,3 kB	18.140,0 kB	[Liste der Dateien]
i386	13.393,7 kB	43.664,0 kB	[Liste der Dateien]
ia64	3.588,0 kB	18.188,0 kB	[Liste der Dateien]
kfreebsd-amd64	14.990,1 kB	52.552,0 kB	[Liste der Dateien]
kfreebsd-i386	13.389,8 kB	43.758,0 kB	[Liste der Dateien]
mips	3.583,7 kB	18.156,0 kB	[Liste der Dateien]
mipsel	3.585,1 kB	18.152,0 kB	[Liste der Dateien]
powerpc	15.019,2 kB	46.228,0 kB	[Liste der Dateien]
s390	3.585,8 kB	18.140,0 kB	[Liste der Dateien]
sparc	15.086,1 kB	46.948,0 kB	[Liste der Dateien]