实用编程语言理论基础（原书第2版）

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

---作者简介---<br>罗伯特·哈珀(Robert Harper) 卡内基·梅隆大学计算机科学系教授，他的主要研究兴趣是类型论在编程语言的设计与实现中的应用，以及其元理论的机械化。Harper是Allen Newell卓越研究奖章和Herbert A. Simon卓越教学奖的获得者，并且是ACM会士。<br><br>---译者简介---<br>张昱 博士，中国科学技术大学计算机科学与技术学院、网络空间安全学院副教授。研究兴趣包括程序设计语言、操作系统和并行计算等，特别是面向人工智能和量子计算等新领域的编程系统、软件分析、异构计算与系统优化等。<br><br>胡明哲 中国科学技术大学网络空间安全学院博士研究生。主要研究方向为多语言软件的程序分析。

译者序<br/>第2版前言<br/>第1版前言<br/>第一部分　判断和规则<br/>第1章　抽象语法 2<br/>1.1　抽象语法树 2<br/>1.2　抽象绑定树 4<br/>1.3　注记 8<br/>习题 8<br/>第2章　归纳定义 10<br/>2.1　判断 10<br/>2.2　推理规则 10<br/>2.3　推导 11<br/>2.4　规则归纳 13<br/>2.5　迭代归纳定义和联立归纳定义 14<br/>2.6　用规则定义函数 15<br/>2.7　注记 15<br/>习题 16<br/>第3章　假言判断与一般性判断 17<br/>3.1　假言判断 17<br/>3.1.1　可导性 17<br/>3.1.2　可纳性 18<br/>3.2　假言归纳定义 20<br/>3.3　一般性判断 21<br/>3.4　泛型归纳定义 22<br/>3.5　注记 23<br/>习题 23<br/>第二部分　静态语义和动态语义<br/>第4章　静态语义 28<br/>4.1　语法 28<br/>4.2　类型系统 29<br/>4.3　结构性质 30<br/>4.4　注记 31<br/>习题 31<br/>第5章　动态语义 33<br/>5.1　转换系统 33<br/>5.2　结构化动态语义 34<br/>5.3　上下文动态语义 36<br/>5.4　等式动态语义 37<br/>5.5　注记 39<br/>习题 39<br/>第6章　类型安全 40<br/>6.1　保持性 40<br/>6.2　进展性 41<br/>6.3　运行时错误 42<br/>6.4　注记 43<br/>习题 43<br/>第7章　求值动态语义 44<br/>7.1　求值动态语义 44<br/>7.2　结构化动态语义和求值动态语义<br/>的关系 45<br/>7.3　重温类型安全 45<br/>7.4　成本动态语义 46<br/>7.5　注记 47<br/>习题 47<br/>第三部分　全函数<br/>第8章　函数定义和值 50<br/>8.1　一阶函数 50<br/>8.2　高阶函数 51<br/>8.3　求值动态语义和定义等同 53<br/>8.4　动态作用域 54<br/>8.5　注记 55<br/>习题 55<br/>第9章　高阶递归的系统T 56<br/>9.1　静态语义 56<br/>9.2　动态语义 57<br/>9.3　可定义性 58<br/>9.4　不可定义性 59<br/>9.5　注记 61<br/>习题 61<br/>第四部分　有限数据类型<br/>第10章　积类型 64<br/>10.1　空积与二元积 64<br/>10.2　有限积 65<br/>10.3　原始互递归 66<br/>10.4　注记 67<br/>习题 67<br/>第11章　和类型 69<br/>11.1　空和与二元和 69<br/>11.2　有限和 70<br/>11.3　和类型的应用 71<br/>11.3.1　void和unit 71<br/>11.3.2　布尔类型 72<br/>11.3.3　枚举 72<br/>11.3.4　选择 73<br/>11.4　注记 74<br/>习题 74<br/>第五部分　类型和命题<br/>第12章　构造逻辑 78<br/>12.1　构造语义 78<br/>12.2　构造逻辑 79<br/>12.2.1　可证性 79<br/>12.2.2　证明项 81<br/>12.3　证明的动态语义 82<br/>12.4　命题即类型 83<br/>12.5　注记 83<br/>习题 83<br/>第13章　经典逻辑 85<br/>13.1　经典逻辑 85<br/>13.1.1　可证性和可反驳性 86<br/>13.1.2　证明和反驳 87<br/>13.2　推导消去形式 89<br/>13.3　证明的动态语义 90<br/>13.4　排中律 91<br/>13.5　双重否定翻译 92<br/>13.6　注记 93<br/>习题 94<br/>第六部分　无限数据类型<br/>第14章　泛型编程 96<br/>14.1　引言 96<br/>14.2　多项式类型算子 96<br/>14.3　正类型算子 98<br/>14.4　注记 99<br/>习题 99<br/>第15章　归纳类型与余归纳类型 101<br/>15.1　示例 101<br/>15.2　静态语义 104<br/>15.2.1　类型 104<br/>15.2.2　表达式 105<br/>15.3　动态语义 105<br/>15.4　求解类型等式 106<br/>15.5　注记 107<br/>习题 107<br/>第七部分　变量类型<br/>第16章　多态类型的系统F 110<br/>16.1　多态抽象 110<br/>16.2　多态的可定义性 113<br/>16.2.1　积与和 113<br/>16.2.2　自然数 114<br/>16.3　参数化概述 115<br/>16.4　注记 116<br/>习题 116<br/>第17章　抽象类型 117<br/>17.1　存在类型 117<br/>17.1.1　静态语义 118<br/>17.1.2　动态语义 118<br/>17.1.3　安全性 118<br/>17.2　数据抽象 119<br/>17.3　存在类型的可定义性 120<br/>17.4　表示独立性 120<br/>17.5　注记 122<br/>习题 122<br/>第18章　高阶种类 123<br/>18.1　构造器和种类 123<br/>18.2　构造器等同 125<br/>18.3　表达式和类型 126<br/>18.4　注记 126<br/>习题 127<br/>第八部分　部分性和递归类型<br/>第19章　递归函数的系统PCF 130<br/>19.1　静态语义 131<br/>19.2　动态语义 132<br/>19.3　可定义性 133<br/>19.4　有限数据结构和无限数据结构 135<br/>19.5　完全性与部分性 135<br/>19.6　注记 136<br/>习题 136<br/>第20章　递归类型的系统FPC 138<br/>20.1　求解类型等式 138<br/>20.2　归纳类型和余归纳类型 139<br/>20.3　自指/自引用 141<br/>20.4　状态的起源 142<br/>20.5　注记 143<br/>习题 143<br/>第九部分　动态类型<br/>第21章　无类型的λ演算 146<br/>21.1　λ演算 146<br/>21.2　可定义性 147<br/>21.3　Scott定理 149<br/>21.4　无类型意味着单类型 150<br/>21.5　注记 151<br/>习题 151<br/>第22章　动态定型 153<br/>22.1　动态类型化PCF 153<br/>22.2　变体和扩展 156<br/>22.3　动态定型的批判 158<br/>22.4　注记 158<br/>习题 159<br/>第23章　混合定型 160<br/>23.1　一个混合语言 160<br/>23.2　动态语义作为静态定型 162<br/>23.3　动态定型的优化 162<br/>23.4　静态定型和动态定型的对比 164<br/>23.5　注记 165<br/>习题 165<br/>第十部分　子定型<br/>第24章　结构化子定型 168<br/>24.1　包含规则 168<br/>24.2　各种子定型 169<br/>24.2.1　数值类型 169<br/>24.2.2　积类型 169<br/>24.2.3　和类型 170<br/>24.2.4　动态类型 170<br/>24.3　变体 171<br/>24.3.1　积类型与和类型 171<br/>24.3.2　部分函数类型 171<br/>24.3.3　递归类型 172<br/>24.3.4　量化类型 173<br/>24.4　动态语义和安全性 174<br/>24.5　注记 175<br/>习题 176<br/>第25章　行为定型 177<br/>25.1　静态语义 177<br/>25.2　布尔盲 183<br/>25.3　细化的安全性 184<br/>25.4　注记 185<br/>习题 186<br/>第十一部分　动态分派<br/>第26章　类与方法 188<br/>26.1　分派矩阵 188<br/>26.2　基于类的组织 190<br/>26.3　基于方法的组织 191<br/>26.4　自指 192<br/>26.5　注记 194<br/>习题 194<br/>第27章　继承 196<br/>27.1　类与方法扩展 196<br/>27.2　基于类的继承 197<br/>27.3　基于方法的继承 198<br/>27.4　注记 198<br/>习题 199<br/>第十二部分　控制流<br/>第28章　控制栈 202<br/>28.1　机器定义 202<br/>28.2　安全性 203<br/>28.3　机器K的正确性 204<br/>28.3.1　完备性 205<br/>28.3.2　可靠性 205<br/>28.4　注记 206<br/>习题 207<br/>第29章　异常 208<br/>29.1　失败 208<br/>29.2　异常 209<br/>29.3　异常值 210<br/>29.4　注记 211<br/>习题 211<br/>第30章　延续 213<br/>30.1　概述 213<br/>30.2　延续的动态语义 214<br/>30.3　用延续构造协程 216<br/>30.4　注记 218<br/>习题 218<br/>第十三部分　符号数据<br/>第31章　符号 222<br/>31.1　符号声明 222<br/>31.1.1　有作用域的动态语义 223<br/>31.1.2　无作用域的动态语义 224<br/>31.2　符号引用 224<br/>31.2.1　静态语义 225<br/>31.2.2　动态语义 225<br/>31.2.3　安全性 225<br/>31.3　注记 226<br/>习题 226<br/>第32章　流动绑定 227<br/>32.1 静态语义 227<br/>32.2　动态语义 228<br/>32.3　类型安全 229<br/>32.4　一些微妙之处 229<br/>32.5　流动引用 231<br/>32.6　注记 231<br/>习题 232<br/>第33章　动态分类 233<br/>33.1　动态类 233<br/>33.1.1　静态语义 233<br/>33.1.2　动态语义 234<br/>33.1.3　安全性 234<br/>33.2　类引用 234<br/>33.3　动态类的可定义性 235<br/>33.4　动态分类的应用 236<br/>33.4.1　秘密分类 236<br/>33.4.2　异常值 237<br/>33.5　注记 237<br/>习题 237<br/>第十四部分　可变状态<br/>第34章　现代化的Algol 240<br/>34.1　基本命令 240<br/>34.1.1　静态语义 241<br/>34.1.2　动态语义 241<br/>34.1.3　安全性 243<br/>34.2　一些编程习语 243<br/>34.3　类型化的命令和类型化的可赋值对象 245<br/>34.4　注记 247<br/>习题 247<br/>第35章　可赋值对象的引用 250<br/>35.1　能力 250<br/>35.2　有作用域的可赋值对象 251<br/>35.3　自由的可赋值对象 252<br/>35.4　安全性 254<br/>35.5　良性效应 256<br/>35.6　注记 257<br/>习题 257<br/>第36章　惰性求值 258<br/>36.1　按需的PCF 258<br/>36.2　按需的PCF的安全性 260<br/>36.3　按需的FPC 262<br/>36.4　悬挂类型 263<br/>36.5　注记 264<br/>习题 264<br/>第十五部分　并行<br/>第37章　嵌套并行 268<br/>37.1　二叉fork-join 268<br/>37.2　成本动态语义 270<br/>37.3　多叉fork-join 273<br/>37.4　有界实现 274<br/>37.5　调度 277<br/>37.6　注记 279<br/>习题 279<br/>第38章　未来与投机 280<br/>38.1　未来 280<br/>38.1.1　静态语义 280<br/>38.1.2　顺序动态语义 281<br/>38.2　投机 281<br/>38.2.1　静态语义 81<br/>38.2.2　顺序动态语义 282<br/>38.3　并行动态语义 282<br/>38.4　未来流水线 284<br/>38.5　注记 285<br/>习题 285<br/>第十六部分　并发与分布式<br/>第39章　进程演算 288<br/>39.1　动作与事件 288<br/>39.2　交互 289<br/>39.3　复制 291<br/>39.4　分配通道 292<br/>39.5　通信 294<br/>39.6　通道传递 296<br/>39.7　普适性 297<br/>39.8　注记 299<br/>习题 299<br/>第40章　并发Algol 301<br/>40.1　并发Algol 301<br/>40.2　广播通信 303<br/>40.3　选择性通信 305<br/>40.4　自由的可赋值对象作为进程 307<br/>40.5　注记 308<br/>习题 308<br/>第41章　分布式Algol 309<br/>41.1　静态语义 309<br/>41.2　动态语义 312<br/>41.3　安全性 313<br/>41.4　注记 314<br/>习题 314<br/>第十七部分　模块化<br/>第42章　模块化与链接 316<br/>42.1　简单单元与链接 316<br/>42.2　初始化和效果 317<br/>42.3　注记 318<br/>第43章　单例种类和子种类 319<br/>43.1　概述 319<br/>43.2　单例 320<br/>43.3　依赖种类 322<br/>43.4　高阶单例 324<br/>43.5　注记 325<br/>习题 326<br/>第44章　类型抽象与类型类 327<br/>44.1　类型抽象 328<br/>44.2　类型类 329<br/>44.3　模块语言 331<br/>44.4　一等模块和二等模块 334<br/>44.5　注记 335<br/>习题 335<br/>第45章　层次结构和参数化 337<br/>45.1　层次结构 337<br/>45.2　抽象 339<br/>45.3　层次结构和抽象 341<br/>45.4　应用函子 343<br/>45.5　注记 344<br/>习题 344<br/>第十八部分　等式推理<br/>第46章　系统T的相等性 346<br/>46.1　观测等价 346<br/>46.2　逻辑等价 349<br/>46.3　逻辑等价和观测等价重合 350<br/>46.4　一些相等性定律 352<br/>46.4.1　一般定律 352<br/>46.4.2　相等性定律 353<br/>46.4.3　归纳定律 353<br/>46.5　注记 353<br/>第47章　系统PCF的相等性 354<br/>47.1　观测等价 354<br/>47.2　逻辑等价 354<br/>47.3　逻辑等价和观测等价重合 355<br/>47.4　紧致性 357<br/>47.5　惰性自然数 360<br/>47.6　注记 361<br/>第48章　参数化 362<br/>48.1　概述 362<br/>48.2　观测等价 362<br/>48.3　逻辑等价 364<br/>48.4　参数化性质 368<br/>48.5　重温表示独立性 370<br/>48.6　注记 371<br/>第49章　进程等价 372<br/>49.1　进程演算 372<br/>49.2　强等价 374<br/>49.3　弱等价 376<br/>49.4　注记 377<br/>附录A　有限集的背景 378<br/>参考文献 379