TL;DR
- ML の一種である Objective Caml を題材に、プログラミング言語の意味論、型システム、基礎概念と、それらの間の数学的な関係を学ぶ本である。
- 導出システム入門、ML の操作的意味論、ML の型システムの 3 部で構成される。
対象読者
プログラミング言語の意味論や型システムを、理論から学びたい人に向けた本である。オンライン演習システムがあり、「証明」を解答とする演習問題の正誤を Web 上で自動で判定できる。
目次
第1部 導出システム入門
- 自然数の加算・乗算・比較
- メタ定理と帰納法による証明
第2部 MLの操作的意味論
- 整数・真偽値式の評価
- 定義，変数束縛と環境
- 関数と再帰
- 静的有効範囲と名前無し表現
- リストとパターンマッチング
第3部 MLの型システム
- 単純型システム
- 多相的型システム
- 型推論