Coq参考資料

「Coq参考資料」の編集履歴（バックアップ）一覧に戻る

Coq参考資料 - (2010/02/14 (日) 11:20:09) の編集履歴(バックアップ)

---

Coq参考資料

教科書

• "Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive"
  • Springerから出版されているCoq本。良い本なのだが値段も高い。
• Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/)
  • Harvardの授業で使用 (PDF 360ページ程度)。定期的に改訂されている。 (Latest 2010/2/3)
  • CPDTは関数型言語プログラマにとってCoqを理解しやすいいいテキストだと思います。
  • 読む時は「Certified Programming with Dependent Types関係」も参照の事。

チュートリアル

• The Coq Proof Assistant, A Tutorial (http://coq.inria.fr/V8.1/files/doc/Tutorial.pdf)
  • Coqを使って簡単な証明をするサンプル多め。(44 pages)
• Coq in a Hurry (http://cel.archives-ouvertes.fr/docs/00/33/44/28/PDF/coq-hurry.pdf)
  • Coqの概要を一通り知るには短くて良いかも。(22 pages)

日本語で読める資料

• 名古屋大学 講義資料 「数理解析・計算機数学 III」 (下記リンクの下の方) (http://www.math.nagoya-u.ac.jp/~garrigue/lecture/2009_AW/index.html)
• お茶の水女子大学 Coqゼミ資料 (下記リンクの真ん中辺り) (http://pllab.is.ocha.ac.jp/lab.html)
• にわとり小屋でのプログラミング日記 (http://d.hatena.ne.jp/yoshihiro503/)
• Coq を使った証明 : まとめ (http://www.kmonos.net/pub/Presen/coq-matome.ppt)

---

その他

カリー＝ハワード対応の話

この辺りが概要を掴むのに良いかと。

• http://www.kmonos.net/wlog/61.html#_0538060508
• http://www.kmonos.net/wlog/61.html#_1826060509