[  sarge  ] [  etch  ] [  etch-m68k  ] [  lenny  ] [  sid  ] [  experimental  ]
[ Quellcode: coq  ]

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

proof assistant for higher-order logic (toplevel and compiler)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp4. For more information, see <http://coq.inria.fr/>.

This packages provides coqtop, a command line interface to Coq.

A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be edited using emacs and xemacs. This requires the proofgeneral-coq package to be installed.

Markierungen: Software-Entwicklung: Compiler, Feld: Mathematik, Implementiert in: OCaml, Benutzer-Schnittstellen: Kommandozeile, Text-basiert interaktiv, Rolle: Programm, Scope: Hilfswerkzeug, Interface Toolkit: 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
    Common facilities for all emacsen
  • dep: hurd [hurd-i386]
    GNU Hurd
  • dep: libc0.1 (>= 2.7-1) [kfreebsd-amd64, kfreebsd-i386]
    GNU C-Bibliothek: Dynamische Bibliotheken
    auch ein virtuelles Paket, bereitgestellt durch libc0.1-udeb
  • dep: libc0.3 (>= 2.7-1) [hurd-i386]
    GNU C-Bibliothek: Dynamische Bibliotheken
    auch ein virtuelles Paket, bereitgestellt durch libc0.3-udeb
  • dep: libc6 (>= 2.5-5) [m68k]
    GNU C-Bibliothek: Dynamische Bibliotheken
    auch ein virtuelles Paket, bereitgestellt durch libc6-udeb
    dep: libc6 (>= 2.7-1) [nicht alpha, hurd-i386, ia64, kfreebsd-amd64, kfreebsd-i386, m68k]
  • 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) [nicht hurd-i386]
    common infrastructure for building and installing TeX
    dep: tex-common (>= 1.11) [hurd-i386]
  • 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]
hurd-i386 8.1.pl3+dfsg-1 8 213,1 kB30412 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]
kfreebsd-amd64 (inoffizielle Portierung) 8.1.pl3+dfsg-1+b2 4 166,9 kB19216 kB [Liste der Dateien]
kfreebsd-i386 (inoffizielle Portierung) 8.1.pl3+dfsg-1+b2 8 258,0 kB30720 kB [Liste der Dateien]
m68k 8.1.pl3+dfsg-1+b2 4 014,9 kB18580 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]