Coqの入門記事を書く会 (4)
今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。
英語
言語そのものを浅く/深く眺めていく、という方向のテキスト3つ:
- 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の良い上手い使い方を学ぶ」ための本。
- 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
- あろはさんによる大量の解説付きで本家チュートリアルを読む連載