Coq

Coq (コック)

総本家: http://coq.inria.fr/

定理証明器(Theorem Prover)や、証明支援系(Proof Assistant)と呼ばれるツールの一つ。

HaskellやMLなどによく似ているが、より強い型システム((Predicative) Calculus of ((Co)Inductive) Construction)を持っているため、依存型やfirst-class多相を実現している。

さらに、Curry-Howard対応により論理式(Higher-Order Intuitive Logic)を扱うことができ、形式的な証明を構築することが出来る。これによって、プログラムを静的に検証することができ、バグのないプログラムを実装することを可能としている。

また、Coq内で作られた関数から、OCaml,Haskell,Schemeといった関数型プログラミング言語のソースコードを得ることができる(Extraction機能)ため、既存のライブラリなどとの連携が容易である。

Coqはフランス語で雄鶏（オスのにわとり）という意味を持つ。

• Coqで四色定理
• CoqでC言語コンパイラの正しさを証明
• Coqで代数学の基本定理