本书给出分析程序设计语言语法性质、操作性质和语义性质的一个框架，该框架基于λ演算系统。全书主要围绕着一系列的λ演算来组织，该系列中λ演算的类型系统依次变得越来越复杂，这些λ演算用来分析和讨论相应的程序设计语言概念，如多态性、抽象数据类型、依赖类型、子定型等。以类型系统为中心对程序设计语言进行的这种研究，在软件工程、语言设计、高性能编译器、高可信软件和形式程序验证等方面有着重要应用。

本书可作为高等院校计算机科学及相关专业的研究生教材，也可供计算机软件工程高级技术人员参考。

第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 类型推断算法
  习题
参考文献