Computing Atlas

How Computing Was Built
Sign In
Text size
100%
Theme

Switch Atlas

Programming Language

Coq (proof assistant)

Functional Language

Coq is an interactive theorem prover and functional programming language based on the calculus of inductive constructions, developed beginning in 1984 at INRIA in France by a team including Thierry Coquand and Gerard Huet. Coq allows a user to write mathematical definitions, state formal theorems, and construct machine-checked proofs of those theorems, with programs and their correctness proofs expressed within the same dependently typed functional language; Coq has been used to formally verify substantial pieces of software and mathematics, including the CompCert verified C compiler and a machine-checked proof of the four color theorem.

Facts
First Released
1989 1
Significance
Used to program and prove correct the CompCert optimizing C compiler. 2
Classification
License
GNU LGPL v2.1 1
Connections

Associated With

Lean (proof assistant), Programming Languages

Sibling interactive proof assistants.

In Field

Formal Methods, Fields
Source Rocq - Wikipedia

Invented By

Christine Paulin-Mohring, Pioneers
Source Rocq - Wikipedia
Gérard Huet, Pioneers
Source Rocq - Wikipedia
Thierry Coquand, Pioneers
Source Rocq - Wikipedia

Licensed Under

GNU Lesser General Public License Version 2.1, Concepts
Sources
1. Wikidata: Rocq prover
  • Wikidata Q1131652, resolved via en.wikipedia pageprops (wave rule R-L)
  • Wikidata Q1131652 P275 (license)
  • Wikidata P577 (publication/release date)
View the Source
2. Rocq - Wikipedia
  • Notable uses, Other applications
    CompCert: an optimizing compiler for almost all of the C programming language which is largely programmed and proven correct in Rocq.
  • In Field: Formal Methods, Lead paragraph
  • Invented By: Thierry Coquand, Infobox: author
    Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, Pierre Castéran
  • Invented By: Gérard Huet, Infobox: author
    Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, Pierre Castéran
  • Invented By: Christine Paulin-Mohring, Infobox: author
    Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, Pierre Castéran
View the Source
Dependent type (Wikipedia)
In Group: Dependently Typed Proof Assistant Languages, article names Rocq (Coq) among functional languages using dependent types to help reduce bugsView the Source
Comments (0)
No comments yet. Be the first to share a thought.
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.