實用編程語言理論基礎（原書第2版） Practical Foundations for Programming Languages

Robert Harper
大學計算機科學系教授，他的主要研究興趣是類型論在編程語言的設計與實現中的應用，以及其元理論的機械化。
Harper是Allen Newell卓越研究獎章和Herbert A. Simon卓越教學獎的獲得者，並且是ACM會士。

---譯者簡介---
張昱 博士
中國科學技術大學計算機科學與技術學院、網絡空間安全學院副教授。
研究興趣包括程序設計語言、操作系統和並行計算等，
特別是面向人工智能和量子計算等新領域的編程系統、軟件分析、異構計算與系統優化等。

胡明哲 
中國科學技術大學網絡空間安全學院博士研究生。
主要研究方向為多語言軟件的程序分析。

譯者序
第2版前言
第1版前言
第一部分 判斷和規則
第1章 抽象語法  2
1.1 抽象語法樹  2
1.2 抽象綁定樹  4
1.3 註記  8
習題  8
第2章 歸納定義  10
2.1 判斷  10
2.2 推理規則  10
2.3 推導  11
2.4 規則歸納  13
2.5 迭代歸納定義和聯立歸納定義  14
2.6 用規則定義函數  15
2.7 註記  15
習題  16
第3章 假言判斷與一般性判斷  17
3.1 假言判斷  17
3.1.1 可導性  17
3.1.2 可納性  18
3.2 假言歸納定義  20
3.3 一般性判斷  21
3.4 泛型歸納定義  22
3.5 註記  23
習題  23
第二部分 靜態語義和動態語義
第4章 靜態語義  28
4.1 語法  28
4.2 類型系統  29
4.3 結構性質  30
4.4 註記  31
習題  31
第5章 動態語義  33
5.1 轉換系統  33
5.2 結構化動態語義  34
5.3 上下文動態語義  36
5.4 等式動態語義  37
5.5 註記  39
習題  39
第6章 類型安全  40
6.1 保持性  40
6.2 進展性  41
6.3 運行時錯誤  42
6.4 註記  43
習題  43
第7章 求值動態語義  44
7.1 求值動態語義  44
7.2 結構化動態語義和求值動態語義
的關係  45
7.3 重溫類型安全  45
7.4 成本動態語義  46
7.5 註記  47
習題  47
第三部分 全函數
第8章 函數定義和值  50
8.1 一階函數  50
8.2 高階函數  51
8.3 求值動態語義和定義等同  53
8.4 動態作用域  54
8.5 註記  55
習題  55
第9章 高階遞歸的系統T  56
9.1 靜態語義  56
9.2 動態語義  57
9.3 可定義性  58
9.4 不可定義性  59
9.5 註記  61
習題  61
第四部分 有限數據類型
第10章 積類型  64
10.1 空積與二元積  64
10.2 有限積  65
10.3 原始互遞歸  66
10.4 註記  67
習題  67
第11章 和類型  69
11.1 空和與二元和  69
11.2 有限和  70
11.3 和類型的應用  71
11.3.1 void和unit  71
11.3.2 布爾類型  72
11.3.3 枚舉  72
11.3.4 選擇  73
11.4 註記  74
習題  74
第五部分 類型和命題
第12章 構造邏輯  78
12.1 構造語義  78
12.2 構造邏輯  79
12.2.1 可證性  79
12.2.2 證明項  81
12.3 證明的動態語義  82
12.4 命題即類型  83
12.5 註記  83
習題  83
第13章 經典邏輯  85
13.1 經典邏輯  85
13.1.1 可證性和可反駁性  86
13.1.2 證明和反駁  87
13.2 推導消去形式  89
13.3 證明的動態語義  90
13.4 排中律  91
13.5 雙重否定翻譯  92
13.6 註記  93
習題  94
第六部分 無限數據類型
第14章 泛型編程  96
14.1 引言  96
14.2 多項式類型算子  96
14.3 正類型算子  98
14.4 註記  99
習題  99
第15章 歸納類型與餘歸納類型  101
15.1 示例  101
15.2 靜態語義  104
15.2.1 類型  104
15.2.2 表達式  105
15.3 動態語義  105
15.4 求解類型等式  106
15.5 註記  107
習題  107
第七部分 變量類型
第16章 多態類型的系統F  110
16.1 多態抽象  110
16.2 多態的可定義性  113
16.2.1 積與和  113
16.2.2 自然數  114
16.3 參數化概述  115
16.4 註記  116
習題  116
第17章 抽像類型  117
17.1 存在類型  117
17.1.1 靜態語義  118
17.1.2 動態語義  118
17.1.3 安全性  118
17.2 數據抽象  119
17.3 存在類型的可定義性  120
17.4 表示獨立性  120
17.5 註記  122
習題  122
第18章 高階種類  123
18.1 構造器和種類  123
18.2 構造器等同  125
18.3 表達式和類型  126
18.4 註記  126
習題  127
第八部分 部分性和遞歸類型
第19章 遞歸函數的系統PCF  130
19.1 靜態語義  131
19.2 動態語義  132
19.3 可定義性  133
19.4 有限數據結構和無限數據結構  135
19.5 完全性與部分性  135
19.6 註記  136
習題  136
第20章 遞歸類型的系統FPC  138
20.1 求解類型等式  138
20.2 歸納類型和余歸納類型  139
20.3 自指/自引用  141
20.4 狀態的起源  142
20.5 註記  143
習題  143
第九部分 動態類型
第21章 無類型的λ演算  146
21.1 λ演算  146
21.2 可定義性  147
21.3 Scott定理  149
21.4 無類型意味著單類型  150
21.5 註記  151
習題  151
第22章 動態定型  153
22.1 動態類型化PCF  153
22.2 變體和擴展  156
22.3 動態定型的批判  158
22.4 註記  158
習題  159
第23章 混合定型  160
23.1 一個混合語言  160
23.2 動態語義作為靜態定型  162
23.3 動態定型的優化  162
23.4 靜態定型和動態定型的對比  164
23.5 註記  165
習題  165
第十部分 子定型
第24章 結構化子定型  168
24.1 包含規則  168
24.2 各種子定型  169
24.2.1 數值類型  169
24.2.2 積類型  169
24.2.3 和類型  170
24.2.4 動態類型  170
24.3 變體  171
24.3.1 積類型與和類型  171
24.3.2 部分函數類型  171
24.3.3 遞歸類型  172
24.3.4 量化類型  173
24.4 動態語義和安全性  174
24.5 註記  175
習題  176
第25章 行為定型  177
25.1 靜態語義  177
25.2 布爾盲  183
25.3 細化的安全性  184
25.4 註記  185
習題  186
第十一部分 動態分派
第26章 類與方法  188
26.1 分派矩陣  188
26.2 基於類的組織  190
26.3 基於方法的組織  191
26.4 自指  192
26.5 註記  194
習題  194
第27章 繼承  196
27.1 類與方法擴展  196
27.2 基於類的繼承  197
27.3 基於方法的繼承  198
27.4 註記  198
習題  199
第十二部分 控制流
第28章 控制棧  202
28.1 機器定義  202
28.2 安全性  203
28.3 機器K的正確性  204
28.3.1 完備性  205
28.3.2 可靠性  205
28.4 註記  206
習題  207
第29章 異常  208
29.1 失敗  208
29.2 異常  209
29.3 異常值  210
29.4 註記  211
習題  211
第30章 延續  213
30.1 概述  213
30.2 延續的動態語義  214
30.3 用延續構造協程  216
30.4 註記  218
習題  218
第十三部分 符號數據
第31章 符號  222
31.1 符號聲明  222
31.1.1 有作用域的動態語義  223
31.1.2 無作用域的動態語義  224
31.2 符號引用  224
31.2.1 靜態語義  225
31.2.2 動態語義  225
31.2.3 安全性  225
31.3 註記  226
習題  226
第32章 流動綁定  227
32.1 靜態語義  227
32.2 動態語義  228
32.3 類型安全  229
32.4 一些微妙之處  229
32.5 流動引用  231
32.6 註記  231
習題  232
第33章 動態分類  233
33.1 動態類  233
33.1.1 靜態語義  233
33.1.2 動態語義  234
33.1.3 安全性  234
33.2 類引用  234
33.3 動態類的可定義性  235
33.4 動態分類的應用  236
33.4.1 秘密分類  236
33.4.2 異常值  237
33.5 註記  237
習題  237
第十四部分 可變狀態
第34章 現代化的Algol  240
34.1 基本命令  240
34.1.1 靜態語義  241
34.1.2 動態語義  241
34.1.3 安全性  243
34.2 一些編程習語  243
34.3 類型化的命令和類型化的可賦值對象  245
34.4 註記  247
習題  247
第35章 可賦值對象的引用  250
35.1 能力  250
35.2 有作用域的可賦值對象  251
35.3 自由的可賦值對象  252
35.4 安全性  254
35.5 良性效應  256
35.6 註記  257
習題  257
第36章 惰性求值  258
36.1 按需的PCF  258
36.2 按需的PCF的安全性  260
36.3 按需的FPC  262
36.4 懸掛類型  263
36.5 註記  264
習題  264
第十五部分 並行
第37章 嵌套並行  268
37.1 二叉fork-join  268
37.2 成本動態語義  270
37.3 多叉fork-join  273
37.4 有界實現  274
37.5 調度  277
37.6 註記  279
習題  279
第38章 未來與投機  280
38.1 未來  280
38.1.1 靜態語義  280
38.1.2 順序動態語義  281
38.2 投機  281
38.2.1 靜態語義  281
38.2.2 順序動態語義  282
38.3 並行動態語義  282
38.4 未來流水線  284
38.5 註記  285
習題  285
第十六部分 並發與分佈式
第39章 進程演算  288
39.1 動作與事件  288
39.2 交互  289
39.3 複製  291
39.4 分配通道  292
39.5 通信  294
39.6 通道傳遞  296
39.7 普適性  297
39.8 註記  299
習題  299
第40章 並發Algol  301
40.1 並發Algol  301
40.2 廣播通信  303
40.3 選擇性通信  305
40.4 自由的可賦值對像作為進程  307
40.5 註記  308
習題  308
第41章 分佈式Algol  309
41.1 靜態語義  309
41.2 動態語義  312
41.3 安全性  313
41.4 註記  314
習題  314
第十七部分 模塊化
第42章 模塊化與鏈接  316
42.1 簡單單元與鏈接  316
42.2 初始化和效果  317
42.3 註記  318
第43章 單例種類和子種類  319
43.1 概述  319
43.2 單例  320
43.3 依賴種類  322
43.4 高階單例  324
43.5 註記  325
習題  326
第44章 類型抽象與類型類  327
44.1 類型抽象  328
44.2 類型類  329
44.3 模塊語言  331
44.4 一等模塊和二等模塊  334
44.5 註記  335
習題  335
第45章 層次結構和參數化  337
45.1 層次結構  337
45.2 抽象  339
45.3 層次結構和抽象  341
45.4 應用函子  343
45.5 註記  344
習題  344
第十八部分 等式推理
第46章 系統T的相等性  346
46.1 觀測等價  346
46.2 邏輯等價  349
46.3 邏輯等價和觀測等價重合  350
46.4 一些相等性定律  352
46.4.1 一般定律  352
46.4.2 相等性定律  353
46.4.3 歸納定律  353
46.5 註記  353
第47章 系統PCF的相等性  354
47.1 觀測等價  354
47.2 邏輯等價  354
47.3 邏輯等價和觀測等價重合  355
47.4 緊緻性  357
47.5 惰性自然數  360
47.6 註記  361
第48章 參數化  362
48.1 概述  362
48.2 觀測等價  362
48.3 邏輯等價  364
48.4 參數化性質  368
48.5 重溫表示獨立性  370
48.6 註記  371
第49章 進程等價  372
49.1 進程演算  372
49.2 強等價  374
49.3 弱等價  376
49.4 註記  377
附錄A 有限集的背景  378
參考文獻  379