第1章 引论
1.1 计算机科学中的类型
1.2 类型系统的优点
1.3 类型系统和语言设计
1.4 历史概要
1.5 相关阅读
第2章 数学基础
2.1 集合、关系和函数
2.2 有序集合
2.3 序列
2.4 归纳
2.5 背景知识阅读
第一部分 无类型系统
第3章 无类型算术表达式
3.1 导论
3.2 语法
3.3 对项的归纳
3.4 语义形式
3.5 求值
3.6 注释
第4章 算术表达式的一个ML实现
4.1 语法
4.2 求值
4.3 其余部分
第5章 无类型lambda演算
5.1 基础
5.2 lambda演算中的程序设计
5.3 形式性
5.4 注释
第6章 项的无名称表示
6.1 项和上下文
6.2 移位和代换
6.3 求值
第7章 lambda演算的一个ML实现
7.1 项和上下文
7.2 移位和代换
7.3 求值
7.4 注释
第二部分 简 单 类 型
第8章 类型算术表达式
8.1 类型
8.2 类型关系
8.3 安全性=进展+保持
第9章 简单类型的lambda演算
9.1 函数类型
9.2 类型关系
9.3 类型的性质
9.4 Curry-Howard对应
9.5 抹除和类型性
9.6 Curry形式和Church形式
9.7 注释
第10章 简单类型的ML实现
10.1 上下文
10.2 项和类型
10.3 类型检查
第11章 简单扩展
11.1 基本类型
11.2 单位类型
11.3 导出形式：序列和通配符
11.4 归属
11.5 let绑定
11.6 序对
11.7 元组
11.8 记录
11.9 和
11.10 变式
11.11 一般递归
11.12 列表
第12章 规范化
12.1 简单类型的规范化
12.2 注释
第13章 引用
13.1 引言
13.2 类型化
13.3 求值
13.4 存储类型
13.5 安全性
13.6 注释
第14章 异常
14.1 提升异常
14.2 处理异常
14.3 带值的异常
第三部分 子类型化
第四部分 递归类型
附录A 部分习题解答
附录B 标记约定
参考文献