Coq

Coq on funktionaalisen ohjelmointiin perustuva todistusapuri. Sen avulla voidaan laatia formaaleja matemaattisia todistuksia, jotka tarkistetaan automaattisesti. Todistukset esitetään induktiivisten konstruktioiden kalkyyliin perustuvalla Gallina-ohjelmointikielellä.

Coqia käytetään mm. ohjelmistojen verifiointiin ja matematiikan formalisointiin. Coq on toteutettu OCaml-kielellä.

Koodiesimerkkejä 
Määritellään luonnollisten lukujen tyyppi:Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.Määritellään luonnollisten lukujen yhteenlasku:Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.Osoitetaan, että määritellylle yhteenlaskufunktiolle pätee  kaikilla .Theorem plus_n_O: forall n: nat, plus n O = n.
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - trivial. simpl. rewrite IHn. reflexivity.
Qed.

Merkittäviä sovellutuksia 
 Neliväriteoreeman Coq-todistus (2005)
 Feitin-Thompsonin lauseen Coq-todistus (2012)
 CompCert: Coqilla toteutettu ja verifioitu C-ohjelmointikielen kääntäjä.

Lähteet

Aiheesta muualla 
 Coqin kotisivu

Ohjelmointi