[  etch  ] [  etch-m68k  ] [  lenny  ] [  squeeze  ] [  sid  ]
[ Quellcode: coq  ]

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

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

  • hängt ab von
  • empfiehlt
  • schlägt vor
  • 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-Bibliothek: Dynamische Bibliotheken
    auch ein virtuelles Paket, bereitgestellt durch libc6-udeb
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    GNU C-Bibliothek: Dynamische Bibliotheken
    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
    line editor for interactive programs
  • 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 kB19404 kB [Liste der Dateien]
amd64 8.1.pl3+dfsg-1+b2 8 825,9 kB33696 kB [Liste der Dateien]
arm 8.1.pl3+dfsg-1+b2 4 091,6 kB18804 kB [Liste der Dateien]
armel 8.1.pl3+dfsg-1+b2 4 116,3 kB18864 kB [Liste der Dateien]
hppa 8.1.pl3+dfsg-1+b2 4 180,0 kB18988 kB [Liste der Dateien]
i386 8.1.pl3+dfsg-1+b2 8 264,1 kB30272 kB [Liste der Dateien]
ia64 8.1.pl3+dfsg-1+b2 4 370,6 kB20380 kB [Liste der Dateien]
mips 8.1.pl3+dfsg-1+b2 4 145,0 kB19336 kB [Liste der Dateien]
mipsel 8.1.pl3+dfsg-1+b2 4 132,1 kB19316 kB [Liste der Dateien]
powerpc 8.1.pl3+dfsg-1+b2 9 236,7 kB32096 kB [Liste der Dateien]
s390 8.1.pl3+dfsg-1+b2 4 226,0 kB19076 kB [Liste der Dateien]
sparc 8.1.pl3+dfsg-1+b2 9 245,7 kB32372 kB [Liste der Dateien]