Coq本家。

coq artってやつですね。こいつが鉄板なんだろうか。積読です。

コンパクトなcoq入門すかね、日本語だと初のCoq本らしいっす。プログラム検証って感じではない。

Emacs上のCoqフロントエンド。Generalの顔が怖い！

下の方。

Coqゼミのコーナーがあります。

大学生によるCoqチュートリアル。

日本語のリファレンス。途中。

TAPLのBenjamin C. Pierceさんの電子ブック。教科書らしい。このコースは以下のことをするとのこと。
「It develop basic concepts of functional programming, logic, operational semantics, lambda-calculus, and static type systems, using the Coq proof assistant.」
読んでみたい。