Types and Programming Languages

この本について

Benjamin C. Pierce 著。型システムについての本。MIT Press、2002年。型システムというのはプログラムの正しさを保証するための形式的な手法である。ここでプログラムの正しさ、というのはプログラミング言語がどのような状況をエラーとするかに依るので一概にいい切れないことに注意。

この本ではまず型なしのシステムから始まり、単純な型のついたシステムとさまざまなデータ構造の型について見てゆき、部分型（subtype）、再帰型（recursive type）、ポリモーフィズム、型オペレータ（type operator）……と見ていく（らしい。訳語は間違ってるかも）。

ホームページ | Bibliography

進め方

1章から順に読んでいく。書き残すべきことのある章だけメモを残す（なので、OCaml による実装の章は飛ばすかもしれない）。練習問題については、Recommended とあるものはできるだけ挑戦する。

目次

• 1. Introduction
• 3. Untyped Arithmetic Expressions
• 5. The Untyped Lambda-Calculus
• 6. Nameless Representation of Terms