対話型定理証明ツール Coq (cockerel) のバージョン 8.12 がリリースされました (ニュース執筆時点で利用可能な最新のマイナー バージョンは 8.12.1)。
Coq には、構成計算理論に基づいた Gallina (チキン) 依存型プログラミング言語が含まれています。
Coq システムを使用すると、仕様への適合性の証明とともに、コンピュータで検証可能な定理証明とプログラムの両方を開発できます。
新しいバージョンでは、標準ライブラリとドキュメントが大幅に改善され、多くのエラーも修正されました。
出所： linux.org.ru