coq

Coq

Coq

Coq (コック)

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

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

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

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

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

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

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

* はてなダイアリーキーワード:Coq