*** Welcome to piglix ***

Coq proof assistant

Coq (software)
Coq logo.png
Developer(s) The Coq development team
Initial release May 1, 1989; 29 years ago (1989-05-01) (version 4.10)
Stable release
8.8.0 / April 17, 2018 (2018-04-17)
Repository github.com/coq/coq
Written in OCaml
Operating system Cross-platform
Available in English
Type Proof assistant
License LGPL 2.1
Website coq.inria.fr
Coq (programming language)
Paradigm Functional
First appeared 1984
Typing discipline static, strong
Filename extensions .v
Website coq.inria.fr
Dialects
LEGO (proof assistant)
Influenced by
ML (programming), LCF (proof methods), Automath (hybrid programming/proving), System F and intuitionistic type theory (language)
Influenced
Agda, Idris, Matita, Albatross

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.

The Association for Computing Machinery rewarded Thierry Coquand, Gérard Pierre Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre Castéran with the 2013 ACM Software System Award for Coq.

Seen as a programming language, Coq implements a dependently typed functional programming language, while seen as a logical system, it implements a higher-order type theory. The development of Coq has been supported since 1984 by INRIA, now in collaboration with École Polytechnique, University of Paris-Sud, Paris Diderot University and CNRS. In the 1990s, École Normale Supérieure de Lyon was also part of the project. The development of Coq was initiated by Gérard Pierre Huet and Thierry Coquand, after which more than 40 people, mainly researchers, contributed features of the core system. The implementation team was successively coordinated by Gérard Pierre Huet, Christine Paulin-Mohring and Hugo Herbelin. Coq is for the most part implemented in OCaml with a bit of C. The core system can be extended thanks to a mechanism of plug-ins.


...
Wikipedia

...