※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

「Coq参考資料」の編集履歴(バックアップ)一覧はこちら

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) 宣言>>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]]
ツールボックス

下から選んでください:

新しいページを作成する
ヘルプ / FAQ もご覧ください。