お勧めの本 - Software Foundations 日本語版Wiki

プログラミング言語の基礎概念

五十嵐淳　サイエンス社 　　ISBN-13: 978-4781912851　　　1850円+税

プログラミング言語OCamlを使用し、プログラムの操作的意味論、型システムの理解を図る。
内容的には一部「Software Foundations」と重なっているところもあり、日本語で書き下されている文書としては非常に貴重。
オンラインで演習問題に取り組むシステムが提供されており、これが非常に出来がいい。ランキングなども表示され、自分がどのあたりにいるかわかる。演習問題のうちの何割かは「修行」とも「イジメ」とも思えるほどのもので、何度も泣きそうになりながら取り組んでいるが、このランキングがなければとっくに投げ出していたかも。
⇒ 2011年9月20日、なんとか演習問題150問をコンプリートしました！！43日かかりました。翻訳ほっぽらかしてやってしまいました。

入門！論理学(中公新書)

野矢茂樹　中央公論新社　　 ISBN-13: 978-4121018625　　　800円ぐらい

題名どおり論理学の入門書ですが、普通の教科書ではサラッと切り上げるようなところにしつこく斬り込んでいくところがなかなか面白いです。

抽象によるソフトウェア設計　Alloyではじめる形式手法

Daniel Jackson著 　オーム社　4500円
形式手法、という言葉に反応して、ちょっと高価ですが買ってみました。あまり厳格さを追い求めず、より現実的なポイントで折り合いをつけて形式手法を導入する、一つの設計の形というところでしょうか。「序文」～「はじめに」のあたりの熱い論調を読むだけでもいろいろと考えさせるとことの多い本です。
ただし、概論が終わって文法や概念の詳説に入ると急に難度が上がります。

プログラム仕様記述論

荒木啓二郎 張 漢明著　オーム社　　2800円
Software Foundationsの後半にホーア論理というものが出てくるのですが、そのへんに入っていく前に何か教科書的なものを読んでおこうと思って買った本です。上のAlloy本よりも厳格で妥協がなく、読み進めるのに非常なエネルギーを必要とします。

無限論の教室

野矢茂樹　講談社現代新書　720円
自然数、実数、集合論に関する無限についての話から始まり、直感主義、形式主義を経てゲーデルに至る、論理学と無限に関する入門書。先にあげた「入門！論理学」と同じ著者だが、こちらのほうが遊びが沢山あって読みやすい。風変わりな大学の先生と男女の生徒二人の講義仕立てになっていて、台詞回しなど明らかに「数学ガール」よりも出来がいいと思う。内容もこの著者ゆえただの入門書というわけではなく、一般的な数学が扱う無限とは異なる見解が入っていて最後まで飽きさせない。

プログラミングの魔道書 Vol.2

株式会社ロングゲート　書籍版2000円 PDF版1500円
ISBN:978-4-9905296-2-8
PDF版は以下のURLでオンライン販売されている
http://longgate.co.jp/products.html
僕が知らないだけかもしれないが、Coqについて、ちゃんと印刷物としてISBN付きで発行されている日本語の書籍はこれだけではないだろうか。Coqについて書かれているのはこのうち１章だけだが、他に依存型についての章があり、この二つをあわせて読むことでCoqがどのような目的を持った言語かを概観できる。Coqに興味があるなら、まず買って読んで損はない。今興味が沸いてきたなら、今が真夜中でもPDFをダウンロードして読むべきだ。SFを読み始める前に基礎知識をつけておくために、とりかかる前に一読を薦める。