Coq

Registered 2009-03-10 by Samuel Bronson

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Project information

Maintainer:
Samuel Bronson
Driver:
Not yet selected
Licence:
GNU LGPL v2.1

RDF metadata

View full history Series and milestones

trunk series is the current focus of development.

All code Code

Version control system:
Bazaar
Programming languages:
ocaml

All packages Packages in Distributions

Get Involved

  • warning
    Report a bug
  • warning
    Ask a question
  • warning
    Help translate

Downloads

Coq does not have any download files registered with Launchpad.