Coq参考資料

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)
  • 日本語によるTutorial解説。最初の部分だけだが、あろはさんによる面白可笑しく懇切丁寧な解説記事。
    • The Coq Proof Assistant A Tutorial (1) 宣言
    • The Coq Proof Assistant A Tutorial (2) 定義
    • The Coq Proof Assistant A Tutorial (3) Minimal Logic
    • The Coq Proof Assistant A Tutorial (4) 自然演繹法
    • The Coq Proof Assistant A Tutorial (5) 自然演繹法 II
    • The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明
    • The Coq Proof Assistant A Tutorial (7) 古典論理
    • The Coq Proof Assistant A Tutorial (8) 一休み
    • The Coq Proof Assistant A Tutorial (9) 排中律の証明
    • The Coq Proof Assistant A Tutorial (10) 二重否定に関する小ネタ
    • The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)
    • The Coq Proof Assistant A Tutorial (12) 述語論理
• Coq in a Hurry (http://cel.archives-ouvertes.fr/docs/00/33/44/28/PDF/coq-hurry.pdf)
  • Coqの概要を一通り知るには短くて良いかも。(22 pages)
  • 最新版はこちら⇒(http://cel.archives-ouvertes.fr/docs/00/45/91/39/PDF/coq-hurry.pdf)ページ数が増えている。
• Coq for POPL Folk
  • POPL 2008でのCoq Tutorialなので、内容もPOPLに来る様な人向けで、"How to write your next POPL paper in Coq" ということらしい。The simply-typed lambda calculusをCoqで、など計算機科学の人には最短コースなのかも。
• Interactive Computer Theorem Proving (CS294-9 Fall 2006) 古い講義資料で、最近はCPDTに乗り換えたらしい。
• Program Verification in Coq プレゼン資料(PDF)。Coqで仕様を書いてプログラムを書くとはどういうことか、割と良く説明してる。

日本語で読める資料

• 名古屋大学 講義資料 「数理解析・計算機数学 III」 (下記リンクの下の方) (http://www.math.nagoya-u.ac.jp/~garrigue/lecture/2009_AW/index.html)
  • 一応全部解答を作ってみました。2010年後期が終わったらここにリンクを作る予定。
• お茶の水女子大学 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)
• Coq クィックリファレンス - まじかんと
• Coq CheatSheet - coqグループ

---

その他

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

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

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

良く薦められている文献はPhil WadlerのProofs are Programs:
19th Century Logic and 21st Century Computing　(PDF)