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

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

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

  • depends
  • recommends
  • suggests
  • 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]
    Biblioteca de C de GNU: Bibliotecas compartidas
    also a virtual package provided by libc6-udeb
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    Biblioteca de C de GNU: Bibliotecas compartidas
    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 kB19404 kB [list of files]
amd64 8.1.pl3+dfsg-1+b2 8,825.9 kB33696 kB [list of files]
arm 8.1.pl3+dfsg-1+b2 4,091.6 kB18804 kB [list of files]
armel 8.1.pl3+dfsg-1+b2 4,116.3 kB18864 kB [list of files]
hppa 8.1.pl3+dfsg-1+b2 4,180.0 kB18988 kB [list of files]
i386 8.1.pl3+dfsg-1+b2 8,264.1 kB30272 kB [list of files]
ia64 8.1.pl3+dfsg-1+b2 4,370.6 kB20380 kB [list of files]
mips 8.1.pl3+dfsg-1+b2 4,145.0 kB19336 kB [list of files]
mipsel 8.1.pl3+dfsg-1+b2 4,132.1 kB19316 kB [list of files]
powerpc 8.1.pl3+dfsg-1+b2 9,236.7 kB32096 kB [list of files]
s390 8.1.pl3+dfsg-1+b2 4,226.0 kB19076 kB [list of files]
sparc 8.1.pl3+dfsg-1+b2 9,245.7 kB32372 kB [list of files]