程序设计语言理论
2010-2
高等教育出版社
陈意云,张昱
350
无
《程序设计语言理论（第2版）》给出分析程序设计语言语法性质、操作性质和语义性质的一个框架，该框架基于λ演算系统。全书主要围绕着一系列的λ演算来组织，该系列中λ演算的类型系统依次变得越来越复杂，这些λ演算用来分析和讨论相应的程序设计语言概念，如多态性、抽象数据类型、依赖类型、子定型等。以类型系统为中心对程序设计语言进行的这种研究，在软件工程、语言设计、高性能编译器、高可信软件和形式程序验证等方面有着重要应用。 《程序设计语言理论（第2版）》可作为高等院校计算机科学及相关专业的研究生教材，也可供计算机软件工程高级技术人员参考。
第1章 引言1.1 基本概念1.1.1 程序设计语言的建模1.1.2 λ表示法1.1.3 符号和约定1.2 等式、归约和语义1.2.1 公理语义1.2.2 操作语义1.2.3 指称语义1.3 类型和类型系统1.3.1 类型和类型系统1.3.2 类型化语言的优点1.4 归纳法1.4.1 表达式上的归纳1.4.2 证明上的归纳1.4.3 良基归纳习题第2章 泛代数和代数数据类型2.1 引言2.2 代数、基调和项2.2.1 代数2.2.2 代数项的语法2.2.3 代数以及项在代数中的解释2.2.4 代换引理2.3 等式、可靠性和完备性2.3.1 等式2.3.2 项代数2.3.3 语义蕴涵和等式证明系统2.3.4 完备性的形式2.3.5 同余、商和演绎完备性2.3.6 非空类别和最小模型完备性2.4 同态和初始性2.4.1 同态和同构2.4.2 初始代数2.5 代数数据类型2.5.1 代数数据类型2.5.2 初始代数语义和数据类型归纳2.5.3 解释没有意义的项2.5.4 错误值的其他解决方法2.6 重写系统2.6.1 基本定义2.6.2 合流性和可证的相等性2.6.3 终止性2.6.4 临界对2.6.5 左线性无重叠重写系统2.6.6 局部合流、终止和合流之间的联系2.6.7 代数数据类型的应用习题第3章 简单类型化λ演算3.1 引言3.2 类型和项3.2.1 类型的语法3.2.2 上下文有关语法3.2.3 λ→项的语法3，2.4 带积、和及其他类型的项3.2.5 定型算法3.3 证明系统3.3.1 等式和理论3.3.2 归约规则3.3.3 有其他规则的归约3.4 通用模型、可靠性和完备性3.4.1 通用模型和项的含义3.4.2 应用结构、外延性和框架3.4.3 环境条件3.4.4 类型可靠性和等式可靠性3.4.5 没有空类型的完备性3.4.6 有空类型的完备性3.4.7 其他类型的通用模型3.5 可计算函数编程语言3.5.1 概述3.5.2 PCF的语法3.5.3 声明和语法美化3.5.4 程序和结果3.5.5 公理语义3.5.6 操作语义3.5.7 由各种形式的语义定义的等价关系3.5.8 记录和n元组3.6 各种归约策略3.6.1 归约策略3.6.2 最左归约和惰性归约3.6.3 并行归约3.6.4 急切归约习题第4章 类型化λ演算的模型4.1 引言4.2 递归函数和不动点算子4.2.1 递归函数和不动点算子4.2.2 有不动点算子的急切归约4.2.3 PCF语言的编程实例4.3 论域理论模型和不动点4.3.1 递归定义和不动点算子4.3.2 完全偏序集合、提升和笛卡儿积4.3.3 连续函数4.3.4 不动点和完备连续层级4.3.5 PCF的CPO模型4.4 不动点归纳习题第5章 命令式程序的语义5.1 引言5.2 Kernel语言5.2.1 存储单元5.2.2 表达式的解释5.2.3 程序状态5.3 操作语义5.3.1 表达式的求值5.3.2 命令的执行5.4 指称语义5.4.1 带状态的类型化λ演算5.4.2 语义函数5.4.3 操作语义和指称语义的等价5.5 Kernel语言的Hoare逻辑5.5.1 一阶断言5.5.2 证明规则5.5.3 可靠性5.5.4 小结习题第6章 递归类型6.1 引言6.2 归纳和余归纳6.2.1 余归纳现象6.2.2 归纳和余归纳指南6.2.3 代数和余代数6.3 递归类型6.3.1 递归类型总览6.3.2 递归的数据结构6.4 归纳类型和余归纳类型6.4.1 归纳类型和余归纳类型总览6.4.2 帮助理解的实例习题第7章 多态性7.1 引言7.1.1 概述7.1.2 类型作为函数变元7.2 直谓式多态演算7.2.1 类型和项的语法7.2.2 和其他形式多态性的比较7.2.3 等式证明和归约7.2.4 ML风格的多态声明7.3 非直谓式多态演算7.3.1 引言7.3.2 非直谓式多态λ演算的表达力7.3.3 归约的终止性7.4 数据抽象和存在类型7.5 类型表达式的分类7.5.1 类型表达式的种类7.5.2 类型表达式的定类与相等7.5.3 项的定型习题第8章 依赖类型8.1 引言8.2 带依赖类型的演算8.2.1 依赖积类型8.2.2 依赖和类型8.3 带依赖类型的程序设计8.3.1 简化DML的实例8.3.2 简化DML的定义8.4 广义积与广义和8.4.1 广义积与广义和概念8.4.2 带广义积与广义和的直谓式演算8.4.3 ML模块语言8.4.4 用积与和来表示模块8.4.5 直谓性以及两个全域之间的联系习题第9章 命题和类型9.1 引言9.2 构造逻辑9.2.1 构造语义9.2.2 构造逻辑9.2.3 命题当作类型9.3 经典逻辑9.3.1 经典逻辑和构造逻辑的区别与联系9.3.2 经典逻辑的规则9.3.3 推导消去形式9.3.4 证明的动态性习题第10章 子定型10.1 引言10.2 有子定型的简单类型化λ演算10.3 记录10.3.1 记录子定型的一般性质10.3.2 带记录和子定型的类型化演算10.4 子定型的语义模型10.4.1 概述10.4.2 子定型的转换解释10.4.3 类型的子集解释10.5 对象的递归记录模型10.5.1 递归记录类型10.5.2 递归类型的子定型习题第11章 类型推断11.1 引言11.2 带类型变量的λ→类型推断11.2.1 语言λt→11.2.2 代换、实例与合一11.2.3 主定型算法11.2.4 隐式定型11.2.5 定型和合一的等价11.3 带多态声明的类型推断11.3.1 ML类型推断和多态变量11.3.2 两组隐式定型规则11.3.3 类型推断算法习题参考文献
无