Coqの入門記事を書く会 (4)

今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。

英語

言語そのものを浅く/深く眺めていく、という方向のテキスト３つ：

• Coq in a Hurry
  • 「忙しい人のためのCoq入門」。比較的よくまとまっている気がしました。
• Coq Proof Assistant： A Tutorial
  • 本家のチュートリアル
• Interactive Theorem Proving and Program Development (Coq'Art)
  • Amazon
  • 定番の一冊

講義の素材として作られたチュートリアル達。より具体的な題材での演習付きなので面白いかも：

• 2nd Asian-Pacific Summer School on Formal Methods
• Using Proof Assistants for Programming Language Research or, How to write your next POPL paper in Coq
  • プログラミング言語処理系の検証が題材
• Formal Type Theory
  • 型理論の決定版テキスト Types and Programming Languages をCoqでやる、という講義
• Modelling and verifying algorithms in Coq： an introduction
  • アルゴリズムの検証が題材ですが、大部分はCoqそのもののチュートリアルという感じ

Coqの使い方はわかる、という人が、その先「Coqの良い上手い使い方を学ぶ」ための本。

• Certified Programming with Dependent Types
  • つい先日読んでみたら、とても面白かったです。おすすめ。

日本語

• Coqの入門記事を書く会
  • ここです。
• Anarchy Proof
  • 何度も紹介してますが、ユーザー投稿型Coqの問題集サイト。おすすめです。
• Coq (@as305.dyndns.org)
  • tactic集がわかりやすいです。一度は目を通しておくべき。
• Coq (@eva-01.jp)
  • Curry-Howard対応などのバックグラウンドの解説多め
• にわとり小屋でのプログラミング日記
  • 日本のCoq第一人者yoshihiro503さんのブログ。いろいろな「Coqで書いてみた」が勉強になります
• ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial
  • あろはさんによる大量の解説付きで本家チュートリアルを読む連載