Coqで独習するならどのページがいい？と聞かれたときのメモ

• Download Coq(英語)
  • ダウンロードしなければ何も始まらない。
  • Download | The Coq Proof Assistant
  • ちなみにLinuxディストリならcoqideパッケージをインストールするのが吉
• Coqの入門記事を書く会
  • そこそこ体系的な入門サイト
  • 2010-09-02 - ひとり勉強会
  • 2010-09-14 - ひとり勉強会
  • 2010-09-19 - ひとり勉強会
  • 2010-10-12 - ひとり勉強会
• Coq 99
  • 練習問題。直観主義論理における有名な証明を一通り解ける。
  • Functional Programming Memo: [Coq] Coq-99 : Part 1
• anarchy proof
  • 練習用サイト。途中から一気に難化するのが問題。
  • わからなかったら他の人の解答も見られる
  • anarchy proof -
• Curry-Howard Isomorphism
  • 定理証明の基礎となる概念の説明。kinabaさんによるわかりやすい説明。
  • d.y.d.
• 2009年度後期・数理解析・計算機数学 III
  • 某大学の資料。
  • 「第8回 12月2æ—¥ Coqで関数型プログラミング」以降がCoqの話。ここから読み初めてもわかりやすい。
  • 2009年度後期・数理解析・計算機数学 III
• Coq Tactics(英語)
  • Coqのタクティックス(戦略)一覧。
  • Tactics Index
• Coq Standard Library(英語)
  • Coqのライブラリ(予め証明された定理やデータ型など)一覧。
  • Standard Library | The Coq Proof Assistant
• 連絡先
  • 人に頼ることこそ大事なり
  • Skype: qnighy
  • Twitter: @qnighy
• ついったーのリスト
  • Sign in to Twitter - anarchy proofの利用者リスト。
  • Sign in to Twitter - CoqPartyの参加者リスト。