ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (1) 宣言The Coq Proof Assistant A Tutorial を参考にしつつ，Coq について勉強していこうと思っています． まずは，Windows を使っている人は，ここから， coq-8.0pl3-win.exeをダウンロードして，ダブルクリックして Coq (IDE 付き) をインストールしておいてください． Coq は Calculuc of Inductive Constructions という論理体系に基づいた，定理証明支援系なのだそうです． 対話的に形式的な証明を構成していくことができて，さらにそれを，そのまま関数型プログラムの仕様として扱うことができるとのこと． このチュートリアルでは Gallina と呼ばれる基本的な言語仕様だけを扱うそうで，発展的な情報は Coq Reference Manual とか Coq'Art を参照せよ，とのこと． とりあえず，C:\
