「Coq参考資料」の編集履歴（バックアップ）一覧はこちら
「Coq参考資料」(2010/10/13 (水) 09:45:45) の最新版変更点
追加された行は緑色になります。
削除された行は赤色になります。
*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) 宣言>>http://alohakun.blog7.fc2.com/blog-entry-271.html]]
--- [[The Coq Proof Assistant A Tutorial (2) 定義>>http://alohakun.blog7.fc2.com/blog-entry-273.html]]
--- [[The Coq Proof Assistant A Tutorial (3) Minimal Logic>>http://alohakun.blog7.fc2.com/blog-entry-275.html]]
--- [[The Coq Proof Assistant A Tutorial (4) 自然演繹法>>http://alohakun.blog7.fc2.com/blog-entry-276.html]]
--- [[The Coq Proof Assistant A Tutorial (5) 自然演繹法 II>>http://alohakun.blog7.fc2.com/blog-entry-277.html]]
--- [[The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明>>http://alohakun.blog7.fc2.com/blog-entry-278.html]]
--- [[The Coq Proof Assistant A Tutorial (7) 古典論理>>http://alohakun.blog7.fc2.com/blog-entry-279.html]]
--- [[The Coq Proof Assistant A Tutorial (8) 一休み>>http://alohakun.blog7.fc2.com/blog-entry-281.html]]
--- [[The Coq Proof Assistant A Tutorial (9) 排中律の証明>>http://alohakun.blog7.fc2.com/blog-entry-286.html]]
--- [[The Coq Proof Assistant A Tutorial (10) 二重否定に関する小ネタ>>http://alohakun.blog7.fc2.com/blog-entry-289.html]]
--- [[The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)>>http://alohakun.blog7.fc2.com/blog-entry-290.html]]
--- [[The Coq Proof Assistant A Tutorial (12) 述語論理>>http://alohakun.blog7.fc2.com/blog-entry-291.html]]
- 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>>http://www.cis.upenn.edu/~plclub/popl08-tutorial/code/index.html]]
-- 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)>>http://adam.chlipala.net/itp/]] 古い講義資料で、最近はCPDTに乗り換えたらしい。
- [[Program Verification in Coq>>http://wiki.di.uminho.pt/twiki/pub/Education/MapiFc/0809/L8psvc.pdf]] プレゼン資料(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)
----
**その他
***カリー＝ハワード対応の話
日本語だとこの辺りが概要を掴むのに良いかと。
- 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)>>http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf]]
*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) 宣言>>http://alohakun.blog7.fc2.com/blog-entry-271.html]]
--- [[The Coq Proof Assistant A Tutorial (2) 定義>>http://alohakun.blog7.fc2.com/blog-entry-273.html]]
--- [[The Coq Proof Assistant A Tutorial (3) Minimal Logic>>http://alohakun.blog7.fc2.com/blog-entry-275.html]]
--- [[The Coq Proof Assistant A Tutorial (4) 自然演繹法>>http://alohakun.blog7.fc2.com/blog-entry-276.html]]
--- [[The Coq Proof Assistant A Tutorial (5) 自然演繹法 II>>http://alohakun.blog7.fc2.com/blog-entry-277.html]]
--- [[The Coq Proof Assistant A Tutorial (6) トートロジーの自動証明>>http://alohakun.blog7.fc2.com/blog-entry-278.html]]
--- [[The Coq Proof Assistant A Tutorial (7) 古典論理>>http://alohakun.blog7.fc2.com/blog-entry-279.html]]
--- [[The Coq Proof Assistant A Tutorial (8) 一休み>>http://alohakun.blog7.fc2.com/blog-entry-281.html]]
--- [[The Coq Proof Assistant A Tutorial (9) 排中律の証明>>http://alohakun.blog7.fc2.com/blog-entry-286.html]]
--- [[The Coq Proof Assistant A Tutorial (10) 二重否定に関する小ネタ>>http://alohakun.blog7.fc2.com/blog-entry-289.html]]
--- [[The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)>>http://alohakun.blog7.fc2.com/blog-entry-290.html]]
--- [[The Coq Proof Assistant A Tutorial (12) 述語論理>>http://alohakun.blog7.fc2.com/blog-entry-291.html]]
- 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>>http://www.cis.upenn.edu/~plclub/popl08-tutorial/code/index.html]]
-- 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)>>http://adam.chlipala.net/itp/]] 古い講義資料で、最近はCPDTに乗り換えたらしい。
- [[Program Verification in Coq>>http://wiki.di.uminho.pt/twiki/pub/Education/MapiFc/0809/L8psvc.pdf]] プレゼン資料(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 クィックリファレンス - まじかんと>>http://homepage2.nifty.com/magicant/programmingmemo/coq/index.html]]
- [[Coq CheatSheet - coqグループ>>http://coq.g.hatena.ne.jp/keyword/CoqCheatSheet]]
----
**その他
***カリー＝ハワード対応の話
日本語だとこの辺りが概要を掴むのに良いかと。
- 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)>>http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf]]
