スマートフォン用の表示で見る

Coq

INRIAで開発されている定理支援証明器。

Gallinaというプログラミング言語で定義を記述し、それに関する性質を証明する支援をしてくれる。

文法はOCamlによく似ている。