内容

目次

第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　多相型レコード計算