Coq参考資料


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

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関係」も参照の事。

チュートリアル

日本語で読める資料



その他

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

日本語だとこの辺りが概要を掴むのに良いかと。
良く薦められている文献はPhil WadlerのProofs are Programs:
19th Century Logic and 21st Century Computing (PDF)
ツールボックス

下から選んでください:

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