第1章 引論
1.1 計算機科學中的類型
1.2 類型係統的優點
1.3 類型係統和語言設計
1.4 曆史概要
1.5 相關閱讀
第2章 數學基礎
2.1 集閤、關係和函數
2.2 有序集閤
2.3 序列
2.4 歸納
2.5 背景知識閱讀
第一部分 無類型係統
第3章 無類型算術錶達式
3.1 導論
3.2 語法
3.3 對項的歸納
3.4 語義形式
3.5 求值
3.6 注釋
第4章 算術錶達式的一個ML實現
4.1 語法
4.2 求值
4.3 其餘部分
第5章 無類型lambda演算
5.1 基礎
5.2 lambda演算中的程序設計
5.3 形式性
5.4 注釋
第6章 項的無名稱錶示
6.1 項和上下文
6.2 移位和代換
6.3 求值
第7章 lambda演算的一個ML實現
7.1 項和上下文
7.2 移位和代換
7.3 求值
7.4 注釋
第二部分 簡 單 類 型
第8章 類型算術錶達式
8.1 類型
8.2 類型關係
8.3 安全性=進展+保持
第9章 簡單類型的lambda演算
9.1 函數類型
9.2 類型關係
9.3 類型的性質
9.4 Curry-Howard對應
9.5 抹除和類型性
9.6 Curry形式和Church形式
9.7 注釋
第10章 簡單類型的ML實現
10.1 上下文
10.2 項和類型
10.3 類型檢查
第11章 簡單擴展
11.1 基本類型
11.2 單位類型
11.3 導齣形式：序列和通配符
11.4 歸屬
11.5 let綁定
11.6 序對
11.7 元組
11.8 記錄
11.9 和
11.10 變式
11.11 一般遞歸
11.12 列錶
第12章 規範化
12.1 簡單類型的規範化
12.2 注釋
第13章 引用
13.1 引言
13.2 類型化
13.3 求值
13.4 存儲類型
13.5 安全性
13.6 注釋
第14章 異常
14.1 提升異常
14.2 處理異常
14.3 帶值的異常
第三部分 子類型化
第四部分 遞歸類型
附錄A 部分習題解答
附錄B 標記約定
參考文獻
· · · · · · (收起)