Coq
CoqはCalculus of constructions(英語版)という高階型システム(Thierry CoquandとGérard Huetが1984年に創始したもので、英語ではCoCと略せてシステム名Coqに至る)に基づく。正しい証明は正しく型がつくラムダ式であるというカリー=ハワード同型対応を利用しているので、Coqの証明言語は型付きラムダ計算の一種である。1991年以降Coqが用いているCalculus of Constructionsの変種は、Christine Paulin-Mohringによるもので、帰納的構成を直接含み、Calculus of Inductive Constructions (CIC)という名前がついている。
Coqには
主張を操作する機能
主張の証明を機械的に検査する機能
形式的証明の探索を支援する機能
依存型を用いたプログラムを記述する機能
実行可能な検証済みプログラムを抽出する機能
がある。
加えてCoqには証明の自動化機能が増えている。中にはomegaタクティクというものがあり、プレスバーガー算術の大部分を決定できる。
Coqの最大の達成の中には、
四色定理: Georges GonthierとBenjamin Wernerによって、完全に機械化された証明が2004年に完了した。
CompCert: C言語のコンパイラで、Coqによって開発され証明がつき、2006年にリリースされた。
Feit-Thompson定理(英語版): Georges Gonthierと彼のグループによって、2012年9月に証明が完了した。
がある。
CoqはGNU LGPLライセンスで配布されているフリーソフトウェアである。