about-coq.html

<#include "incl/macros.html">
<#def TITLE>What is Coq?</#def><#include "incl/header.html">

<div class="framework">
<div class="frameworklabel">Handling proofs and programs</div>
<div class="frameworkcontent">

<p>Coq implements a program specification and mathematical higher-level language called <em>Gallina</em> that is based on an expressive formal language called the <em>Calculus of Inductive Constructions</em> that itself combines both a higher-order logic and a richly-typed functional programming language. Through a <em>vernacular</em> language of commands, Coq allows:</p>

    <ul>
      <li>to define functions or predicates, that can be evaluated efficiently;</li>
      <li>to state mathematical theorems and software specifications;</li>
      <li>to interactively develop formal proofs of these theorems;</li>
      <li>to machine-check these proofs by a relatively small certification "kernel";</li>
      <li>to extract certified programs to languages like OCaml, Haskell or Scheme.</li>
    </ul>

   <p>As a proof development system, Coq provides interactive proof
    methods, decision and semi-decision
    algorithms, and a <em>tactic</em> language for letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available.</p>

    <p> As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros.</p>

</div>

<div class="frameworklinks">
<ul>
<li><a href="/a-short-introduction-to-coq">A short introduction to Coq</a></li>
</ul>
</div>

</div>

<div class="framework">
<div class="frameworklabel">The Coq bundle</div>
<div class="frameworkcontent">

    <p> Coq comes with libraries for efficient arithmetics in N, Z and Q,
    libraries about lists, finite sets and finite maps, libraries on
    abstract sets, relations, classical analysis, etc.</p>

    <p> Coq is released with:</p>
      <ul>

      <li>a graphical user interface based on gtk (CoqIDE) (<a
    href="/refman/practical-tools/coqide.html">see the chapter of the reference manual about CoqIDE</a>),</li>
      <li>documentation tools (<tt>coqdoc</tt> and <tt>coq-tex</tt>) and a statistics tool (<tt>coqwc</tt>),</li>
      <li>dependency and makefile generation tools for Coq
	(<tt>coq_makefile</tt> and <tt>coqdep</tt>),</li>
      <li>a stand-alone proof verifier (<tt>coqchk</tt>).</li>
      </ul>
</div>

<div class="frameworklinks">
<ul>
<li><a href="/download">Get Coq!</a></li>
</ul>
</div>

</div>

<div class="framework">
<div class="frameworklabel">Credits</div>
<div class="frameworkcontent">

    <p>Coq is the result of more than 30 years of research. It started in
    1984 from an implementation of the Calculus of Constructions at
    INRIA-Rocquencourt by Thierry Coquand and Gérard Huet. In 1991,
    Christine Paulin extended it to the Calculus of Inductive
    Constructions.

    All in all, more than 200 people have contributed to the
    development of Coq. The <a href="/coq-team.html">Coq Team</a>
    is responsible for the development of Coq and integration of contributions.
    See <a href="<#CURRENTCREDITSURL>">credits</a> for a detailed list
    of contributors over the years, 
    the <a href="/refman/history.html">history</a>
    and <a href="/refman/changes.html">recent changes</a> chapters in
    the Coq Reference Manual for detailed information about changes in the system 
    or the synthetic <a href="/who-did-what-in-coq">who did what</a>
    table for an overview of the systems contributors.</p>

    <p> Coq is written
    in <a href="https://ocaml.org/index.fr.html">OCaml</a>. It is
    distributed under
    the <a href="http://www.gnu.org/licenses/old-licenses/lgpl-2.1.html">GNU
    Lesser General Public Licence Version 2.1</a> (LGPL).</p>
</div>
</div>

<#include "incl/footer.html">