●譯者序
第2版前言
第1版前言
第一部分 判斷和規則
第1章 抽像語法
1.1 抽像語法樹
1.2 抽像綁定樹
1.3 注記
習題
第2章 歸納定義
2.1 判斷
2.2 推理規則
2.3 推導
2.4 規則歸納
2.5 迭代歸納定義和聯立歸納定義
2.6 用規則定義函數
2.7 注記
習題
第3章 假言判斷與一般性判斷
3.1 假言判斷
3.1.1 可導性
3.1.2 可納性
3.2 假言歸納定義
3.3 一般性判斷
3.4 泛型歸納定義
3.5 注記
習題
第二部分 靜態語義和動態語義
第4章 靜態語義
4.1 語法
4.2 類型繫統
4.3 結構性質
4.4 注記
習題
第5章 動態語義
5.1 轉換繫統
5.2 結構化動態語義
5.3 上下文動態語義
5.4 等式動態語義
5.5 注記
習題
第6章 類型安全
6.1 保持性
6.2 進展性
6.3 運行時錯誤
6.4 注記
習題
第7章 求值動態語義
7.1 求值動態語義
7.2 結構化動態語義和求值動態語義
的關繫
7.3 重溫類型安全
7.4 成本動態語義
7.5 注記
習題
第三部分 全函數
第8章 函數定義和值
8.1 一階函數
8.2 高階函數
8.3 求值動態語義和定義等同
8.4 動態作用域
8.5 注記
習題
第9章 高階遞歸的繫統T
9.1 靜態語義
9.2 動態語義
9.3 可定義性
9.4 不可定義性
9.5 注記
習題
第四部分 有限數據類型
第10章 積類型
10.1 空積
10.2 有限積
10.3 原始互遞歸
10.4 注記
習題
第11章 和類型
11.1 空和
11.2 有限和
11.3 和類型的應用
11.3.1 void和unit
11.3.2 布爾類型
11.3.3 枚舉
11.3.4 選擇
11.4 注記
習題
第五部分 類型和命題
第12章 構造邏輯
12.1 構造語義
12.2 構造邏輯
12.2.1 可證性
12.2.2 證明項
12.3 證明的動態語義
12.4 命題即類型
12.5 注記
習題
第13章 經典邏輯
13.1 經典邏輯
13.1.1 可證性和可反駁性
13.1.2 證明和反駁
13.2 推導消去形式
13.3 證明的動態語義
13.4 排中律
13.5 雙重否定翻譯
13.6 注記
習題
第六部分 無限數據類型
第14章 泛型編程
14.1 引言
14.2 多項式類型算子
14.3 正類型算子
14.4 注記
習題
第15章 歸納類型與餘歸納類型
15.1 示例
15.2 靜態語義
15.2.1 類型
15.2.2 表達式
15.3 動態語義
15.4 求解類型等式
15.5 注記
習題
第七部分 變量類型
第16章 多態類型的繫統F
16.1 多態抽像
16.2 多態的可定義性
16.2.1 積與和
16.2.2 自然數
16.3 參數化概述
16.4 注記
習題
第17章 抽像類型
17.1 存在類型
17.1.1 靜態語義
17.1.2 動態語義
17.1.3 安全性
17.2 數據抽像
17.3 存在類型的可定義性
17.4 表示獨立性
17.5 注記
習題
第18章 高階種類
18.1 構造器和種類
18.2 構造器等同
18.3 表達式和類型
18.4 注記
習題
第八部分 部分性和遞歸類型
第19章 遞歸函數的繫統PCF
19.1 靜態語義
19.2 動態語義
19.3 可定義性
19.4 有限數據結構和無限數據結構
19.5 接近性與部分性
19.6 注記
習題
第20章 遞歸類型的繫統FPC
20.1 求解類型等式
20.2 歸納類型和餘歸納類型
20.3 自指/自引用
20.4 狀態的起源
20.5 注記
習題
第九部分 動態類型
第21章 無類型的λ演算
21.1 λ演算
21.2 可定義性
21.3 Scott定理
21.4 無類型意味著單類型
21.5 注記
習題
第22章 動態定型
22.1 動態類型化PCF
22.2 變體和擴展
22.3 動態定型的批判
22.4 注記
習題
第23章 混合定型
23.1 一個混合語言
23.2 動態語義作為靜態定型
23.3 動態定型的優化
23.4 靜態定型和動態定型的對比
23.5 注記
習題
第十部分 子定型
第24章 結構化子定型
24.1 包含規則
24.2 各種子定型
24.2.1 數值類型
24.2.2 積類型
24.2.3 和類型
24.2.4 動態類型
24.3 變體
24.3.1 積類型與和類型
24.3.2 部分函數類型
24.3.3 遞歸類型
24.3.4 量化類型
24.4 動態語義和安全性
24.5 注記
習題
第25章 行為定型
25.1 靜態語義
25.2 布爾盲
25.3 細化的安全性
25.4 注記
習題
第十一部分 動態分派
第26章 類與方法
26.1 分派矩陣
26.2 基於類的組織
26.3 基於方法的組織
26.4 自指
26.5 注記
習題
第27章 繼承
27.1 類與方法擴展
27.2 基於類的繼承
27.3 基於方法的繼承
27.4 注記
習題
……
