高水準プログラミング言語の基礎理論を型付きラムダ計算を用いて詳細に解説。これら基礎理論の学習を通じて、関数型プログラミング言語の動作やその型システムの原理、さらに、多相型、型推論、継続計算、レコード計算などを含むプログラミング言語の種々の高度な機能の基礎を習得できる。
『情報数学講座 9 プログラミング言語の基礎理論』として1997年初版発行後、以来、長年にわたり多数の読者にご愛読いただいてまいりました。この度、多くの読者からの要望を受け単行本に改装し発行するものです。

▼目次
第1章　プログラミング言語のモデル
1.1　計算モデルの必要性
1.2　本書で使用する集合に関する記法
1.3　言語の文法構造の定義
1.4　型無しラムダ計算

第2章　型付きラムダ計算
2.1　定数と基底型の導入
2.2　単純な型付きラムダ計算Λの定義
2.3　de　Bruijnインデックスと束縛変数に関する約束
2.4　Λの表示的意味論
2.5　Λの公理的意味論
2.6　公理的意味論の健全性と完全性
2.7　Λのモデル間の論理関係
2.8　Λの簡約システム
2.9　Λの操作的意味論

第3章　型付きラムダ計算の拡張
3.1　種々のデータ構造の導入
3.2　再帰的データ型
3.3　再帰的関数の定義
3.4　ユーザ定義のデータ型とパターンマッチング
3.5　手続き型言語機能の導入

第4章　型推論システム
4.1　暗黙に型付けられたラムダ計算
4.2　λの型推論アルゴリズム
4.3　種々のデータ構造への拡張

第5章　多相型言語のモデル
5.1　プログラムの汎用性の表現
5.2　多相型ラムダ計算Λ∀
5.3　Λ∀の表示的意味論
5.4　Λ∀の公理的意味論および簡約関係
5.5　種々のデータ構造の表現
5.6　MLの多相型システム

第6章　レコード計算系の理論
6.1　レコード計算系の登場の背景
6.2　サブタイプを含むレコード計算
6.3　多相型レコード計算