Coq

tools software programming-language logic

依存型に基づいた定理証明支援システム。フランスINRIAで開発され、プログラムの正当性証明に使用される。

Coqの勉強で学習リソースを整理している。

関連研究者

• Emilio Jesús Gallego Arias - Faustの形式的証明プロジェクトに関わっている