本书提出了一种基于类型系统和结构操作语义的编程语言理论。第2版经过全面修订，几乎每章都包含习题，并新增一章讨论类型细化。本书涉及的概念广泛，包括：基本数据类型，多态和抽象类型，动态定型，动态分派，子类型和类型细化，符号和动态分类，并行和成本语义，并发和分布。书中对不同编程语言的特性做了分析、证明和比较，所提供的方法可直接应用于语言的实现、程序推理逻辑的研发以及语言特性的形式化验证，具有较高的实用性。本书不仅可以作为高等学校计算机相关专业的编程语言理论课程教材，也可供相关领域的科研人员和技术人员参考阅读。
译者序
第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
书单推荐
