 | |
 | |
| 作者 | フランス国立情報学自動制御研究所, パリ第7大学, エコール・ポリテクニーク, パリ第11大学, リヨン高等師範学校 |
|---|---|
| 初版 | 4.10 (1989年) |
| 最新版 |
8.19.1
/ 2024年3月4日[1] |
| リポジトリ | |
| プログラミング 言語 | OCaml |
| 対応OS | マルチプラットフォーム |
| 対応言語 | 多言語対応 |
| 種別 | 定理証明支援系 |
| ライセンス | GNU LGPL 2.1 |
| 公式サイト | The Coq Proof Assistant |
Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。
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のチームがSsreflect(small scale reflectionの略)というCoqの拡張を開発している。拡張はreflection用の機能にとどまらず、Coqの多くのタクティクの改良版を提供する上に、証明の保守性を高めるコーディング慣習も含んでいる。 Ssreflectの機能には下のようなものがある。
SsreflectはCeCill-BとCecill-2.0でデュアルライセンスされていて、自由に利用できる。Ssreflectの最新版はCoq 8.4上で動く。[5]
