Paket: coq (8.3.pl4+dfsg-1 und andere)

Links für coq

Debian-Ressourcen:

Quellcode-Paket coq herunterladen:

Betreuer:

Debian OCaml Maintainers (QS-Seite, E-Mail-Archiv)
Ralf Treinen (QS-Seite)
Samuel Mimram (QS-Seite)
Stéphane Glondu (QS-Seite)

Externe Ressourcen:

Homepage [coq.inria.fr]

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 Camlp5.

This package 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 package to be installed.

Markierungen: Software-Entwicklung: Compiler, Feld: Mathematik, Implementiert in: implemented-in::ocaml, interface::commandline, Benutzer-Schnittstellen: Text-basiert interaktiv, Rolle: role::program, scope::utility, 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) [m68k]

Paket nicht verfügbar
dep: coq-theories (= 8.2.pl2+dfsg-2) [hppa, powerpcspe]

proof assistant for higher-order logic (theories)

dep: coq-theories (= 8.3.pl2+dfsg-1) [sparc64]

dep: coq-theories (= 8.3.pl4+dfsg-1) [nicht hppa, m68k, powerpcspe, sparc64]
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: libc0.3 (>= 2.7) [hurd-i386]

Die »Embedded GNU C Library«: Laufzeitbibliotheken
auch ein virtuelles Paket, bereitgestellt durch libc0.3-udeb
dep: libc6 (>= 2.11) [powerpcspe]

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

dep: libc6 (>= 2.2) [hppa]

dep: libc6 (>= 2.5-5) [m68k]

dep: libc6 (>= 2.7) [amd64, armel, i386, powerpc, sparc]
dep: libcoq-ocaml-ehg05 [armel]

virtuelles Paket, bereitgestellt durch libcoq-ocaml
dep: libcoq-ocaml-m0xl3 [amd64, kfreebsd-amd64]

virtuelles Paket, bereitgestellt durch libcoq-ocaml
dep: libcoq-ocaml-nc3h8 [alpha, armhf, ia64, mips, mipsel, s390, s390x, sh4]

virtuelles Paket, bereitgestellt durch libcoq-ocaml
dep: libcoq-ocaml-rn5x5 [sparc64]

virtuelles Paket, bereitgestellt durch libcoq-ocaml
dep: libcoq-ocaml-s00f5 [hurd-i386, i386, kfreebsd-i386, powerpc, sparc]

virtuelles Paket, bereitgestellt durch libcoq-ocaml
dep: libgcc1 (>= 1:4.4.0) [armel]

GCC Support-Bibliothek
dep: libncurses5 (>= 5.6+20071006-3) [m68k]

Gemeinsam benutzte Bibliotheken für Terminalsteuerung
dep: ocaml-base-nox-3.10.2 [m68k]

Paket nicht verfügbar
dep: ocaml-base-nox-3.11.2 [hppa, powerpcspe]

virtuelles Paket, bereitgestellt durch ocaml-base-nox
dep: ocaml-base-nox-3.12.0 [sparc64]

virtuelles Paket, bereitgestellt durch ocaml-base-nox
dep: ocaml-base-nox-3.12.1 [nicht hppa, m68k, powerpcspe, sparc64]

virtuelles Paket, bereitgestellt durch ocaml-base-nox
dep: tex-common (>= 1.10) [m68k]

Gemeinsame Infrastruktur zum Erstellen und Installieren von TeX

rec: coqide [nicht hppa, m68k, powerpcspe, sparc64]

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

oder proofgeneral

generic frontend for proof assistants
rec: coqide [hppa, m68k, powerpcspe, sparc64]

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

oder proofgeneral-coq

generic interface for proof assistants - coq support

sug: cle [m68k]

Paket nicht verfügbar
sug: coq-doc

documentation for Coq
sug: ledit [m68k]

Zeileneditor für interaktive Programme
sug: ledit [nicht m68k]

Zeileneditor für interaktive Programme

oder readline-editor

virtuelles Paket, bereitgestellt durch ledit, rlfe, rlwrap
sug: libcoq-ocaml-dev [nicht m68k]

development libraries and tools for Coq
sug: ocaml-nox [nicht m68k]

ML-Implementierung mit einem klassenbasierten Objektsystem (ohne X)

sug: ocaml-nox (>= 3.08) [m68k]
sug: proofgeneral [nicht hppa, m68k, powerpcspe, sparc64]

generic frontend for proof assistants
sug: proofgeneral-coq [hppa, m68k, powerpcspe, sparc64]

generic interface for proof assistants - coq support
sug: why (>= 2.19) [nicht m68k]

Software verification tool

coq herunterladen

Download für alle verfügbaren Architekturen
Architektur	Version	Paketgröße	Größe (installiert)	Dateien
alpha (inoffizielle Portierung)	8.3.pl4+dfsg-1	1.769,9 kB	8.225,0 kB	[Liste der Dateien]
amd64	8.3.pl4+dfsg-1	5.542,9 kB	18.432,0 kB	[Liste der Dateien]
armel	8.3.pl4+dfsg-1	5.967,2 kB	17.898,0 kB	[Liste der Dateien]
armhf	8.3.pl4+dfsg-1	1.770,7 kB	8.225,0 kB	[Liste der Dateien]
hppa	8.2.pl2+dfsg-2	3.608,8 kB	18.268,0 kB	[Liste der Dateien]
hurd-i386	8.3.pl4+dfsg-1+b1	4.941,7 kB	15.044,0 kB	[Liste der Dateien]
i386	8.3.pl4+dfsg-1	4.946,3 kB	15.045,0 kB	[Liste der Dateien]
ia64	8.3.pl4+dfsg-1+b1	1.770,0 kB	8.225,0 kB	[Liste der Dateien]
kfreebsd-amd64	8.3.pl4+dfsg-1	5.537,4 kB	18.311,0 kB	[Liste der Dateien]
kfreebsd-i386	8.3.pl4+dfsg-1	4.940,5 kB	14.925,0 kB	[Liste der Dateien]
m68k (inoffizielle Portierung)	8.1.pl3+dfsg-1+b2	4.014,9 kB	18.580,0 kB	[Liste der Dateien]
mips	8.3.pl4+dfsg-1	1.768,9 kB	8.225,0 kB	[Liste der Dateien]
mipsel	8.3.pl4+dfsg-1+b1	1.768,6 kB	8.225,0 kB	[Liste der Dateien]
powerpc	8.3.pl4+dfsg-1	5.427,1 kB	15.876,0 kB	[Liste der Dateien]
powerpcspe (inoffizielle Portierung)	8.2.pl2+dfsg-2	3.606,8 kB	18.260,0 kB	[Liste der Dateien]
s390	8.3.pl4+dfsg-1	1.770,0 kB	8.225,0 kB	[Liste der Dateien]
s390x	8.3.pl4+dfsg-1	1.771,4 kB	8.225,0 kB	[Liste der Dateien]
sh4 (inoffizielle Portierung)	8.3.pl4+dfsg-1	1.770,3 kB	8.225,0 kB	[Liste der Dateien]
sparc	8.3.pl4+dfsg-1	5.289,9 kB	15.807,0 kB	[Liste der Dateien]
sparc64 (inoffizielle Portierung)	8.3.pl2+dfsg-1	1.763,2 kB	8.432,0 kB	[Liste der Dateien]