Package: coq (8.1.pl3+dfsg-1 and others)

[ Source: coq  ]

Asistente de pruebas de logica de gran magnitud (alto nivel y compilador)

Coq es un asistente de pruebas de lógica de gran magnitud, que permite el desarrollo de programas informáticos consistentes en su especificación formal. Se desarrolla usando Objective Caml y Camlp4. Para más información véase <http://coq.inria.fr/>.

Este paquete proporciona coqtop, una interfaz de consola a Coq.

Se proporciona una interfaz gráfica a Coq en el paquete coqide. Coq también se puede usar con ProofGeneral, que permite editar las pruebas con emacs y xemacs. Este necesita que esté instalado el paquete proofgeneral-coq.

Tags: Software Development: Compiler, Field: Mathematics, Implemented in: OCaml, User Interface: Command Line, Text-based Interactive, Role: Program, Scope: Utility, Interface Toolkit: Ncurses TUI

Other Packages Related to coq

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

  proof assistant for higher-order logic (theories)

• dep: emacsen-common

  Common facilities for all emacsen

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

  GNU C Library: Shared libraries
  also a virtual package provided by libc6-udeb

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

  GNU C Library: Shared libraries
  also a virtual package provided by libc6.1-udeb

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

  Biblioteca de ayuda de GCC

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

  Bibliotecas compartidas para el tratamiento del terminal

• dep: ocaml-base-nox-3.10.2

  virtual package provided by ocaml-base-nox

• dep: tex-common (>= 1.10)

  common infrastructure for building and installing TeX

• rec: coqide

  proof assistant for higher-order logic (gtk interface)

  or proofgeneral-coq

  generic interface for proof assistants - coq support

• sug: cle

  Envuelve cualquier herramienta de consola con readline

• 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

Download coq

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
alpha	8.1.pl3+dfsg-1+b2	4,238.4 kB	19,404.0 kB	[list of files]
amd64	8.1.pl3+dfsg-1+b2	8,825.9 kB	33,696.0 kB	[list of files]
arm	8.1.pl3+dfsg-1+b2	4,091.6 kB	18,804.0 kB	[list of files]
armel	8.1.pl3+dfsg-1+b2	4,116.3 kB	18,864.0 kB	[list of files]
hppa	8.1.pl3+dfsg-1+b2	4,180.0 kB	18,988.0 kB	[list of files]
i386	8.1.pl3+dfsg-1+b2	8,264.1 kB	30,272.0 kB	[list of files]
ia64	8.1.pl3+dfsg-1+b2	4,370.6 kB	20,380.0 kB	[list of files]
mips	8.1.pl3+dfsg-1+b2	4,145.0 kB	19,336.0 kB	[list of files]
mipsel	8.1.pl3+dfsg-1+b2	4,132.1 kB	19,316.0 kB	[list of files]
powerpc	8.1.pl3+dfsg-1+b2	9,236.7 kB	32,096.0 kB	[list of files]
s390	8.1.pl3+dfsg-1+b2	4,226.0 kB	19,076.0 kB	[list of files]
sparc	8.1.pl3+dfsg-1+b2	9,245.7 kB	32,372.0 kB	[list of files]