#176on PLDB | 33Years Old | 3.6kUsers |

3Books | 27Papers | 5kRepos |

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. Read more on Wikipedia...

- the Coq Wikipedia page
- There are at least 5,206 Coq repos on GitHub
- file extensions for Coq include coq and v
- The Google BigQuery Public Dataset GitHub snapshot shows 793 users using Coq in 1k repos on GitHub
- There are 2,066 members in the Coq subreddit
- Explore Coq snippets on Rosetta Code
- Coq is listed on HOPL
- Pygments supports syntax highlighting for Coq
- GitHub supports syntax highlighting for Coq
- See also: OCaml, Agda, Idris, C, Isabelle
- HTML of this page generated by LanguagePage.ts
- Improve our Coq file

Example from Linguist:

```
Require Import FunctionNinjas.All.
Require Import ListString.All.
Require Import Computation.
Import C.Notations.
Definition error (message : LString.t) : C.t :=
do_call! Command.ShowError message in
ret.
Definition main : C.t :=
call! card_is_valid := Command.AskCard in
if card_is_valid then
call! pin := Command.AskPIN in
match pin with
| None => error @@ LString.s "No PIN given."
| Some pin =>
call! pin_is_valid := Command.CheckPIN pin in
if pin_is_valid then
call! ask_amount := Command.AskAmount in
match ask_amount with
| None => error @@ LString.s "No amount given."
| Some amount =>
call! amount_is_valid := Command.CheckAmount amount in
if amount_is_valid then
call! card_is_given := Command.GiveCard in
if card_is_given then
call! amount_is_given := Command.GiveAmount amount in
if amount_is_given then
ret
else
error @@ LString.s "Cannot give you the amount. Please contact your bank."
else
error @@ LString.s "Cannot give you back the card. Please contact your bank."
else
error @@ LString.s "Invalid amount."
end
else
error @@ LString.s "Invalid PIN."
end
else
error @@ LString.s "Invalid card.".
```

Feature | Supported | Example | Token |
---|---|---|---|

Binary Literals | âœ“ | ||

Integers | âœ“ | ||

Floats | âœ“ | ||

Hexadecimals | âœ“ | ||

Octals | âœ“ |

title | authors | year | publisher |
---|---|---|---|

Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (The MIT Press) | Chlipala, Adam | 2013-12-06T00:00:01Z | The MIT Press |

Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant | Chlipala, Adam | 2022 | MIT Press |

Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System (Computer Engineering) | Boldo, Sylvie and Melquiond, Guillaume | 2017 | ISTE Press - Elsevier |

ballerina.html Â· coq.html Â· coldfusion.html