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
Luokka:Ohjelmointi