类型和程序设计语言

第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  带值的异常
 第三部分  子 类 型 化
 第15章  子类型
 15.1  包含
 15.2  子类型关系
 15.3  子类型化和类型化的性质
 15.4  Top类型和Bottom类型
 15.5  子类型化及其他特征
 15. 6  子类型化的强制语义
 15.7  交叉类型和联合类型
 15.8  注释
 第16章  子类型的元理论
 16.1  算法子类型化
 16.2  算法类型化
 16.3  合类型和交类型
 16.4  算法类型化和Bottom类型
 第17章  子类型化的ML语言实现
 17.1  语法
 17.2  子类型化
 17.3  类型化
 第18章  实例分析:命令式对象
 18.1  什么是面向对象编程
 18.2  对象
 18.3  对象生成器
 18.4  子类型化
 18.5  聚集实例变量
 18.6  简单类
 18.7  添加实例变量
 18.8  调用超类方法
 18.9  含self类
 18.10使用self的开放递归
 18.11开放递归及求值顺序
 18.12更高效的实现
 18.13小结
 18.14注释
 第19章  实例分析:轻量级的Java
 19.1  引言
 19.2  概要
 19.3  规范化和结构化的类型系统
 19.4  定义
 19.5  性质
 19.6  编码及初始对象
 19.7  注释
 第四部分  递 归 类 型
 第20章  递归类型简介
 20.1  实例
 20.2  形式
 20.3  子类型化
 20.4  注释
 第21章  递归类型元理论
 21.1  归纳和共归纳
 21.2  有限类型和无穷类型
 21.3  子类型
 21.4  传递性的偏离
 21.5  成员检查
 21.6  更高效算法
 21.7  正则树
 21.8  μ类型
 21.9  计算子表达式
 21.10关于指数级算法的闲话
 21.11子类型化同构递归类型
 21.12注释第五部分  多    态
 第22章  类型重构
 22.1  类型变量和代换
 22.2  类型变量的两个观点
 22.3  基于约束的类型化
 22.4  合一
 22.5  主类型
 22.6  隐含的类型注释
 22.7  let多态
 22.8  注释
 第23章  全称类型
 23.1  动机
 23.2  各种多态
 23.3  系统F
 23.4  实例
 23.5  基本性质
 23.6  抹除,可类型化,类型重构
 23.7  抹除和求值顺序
 23.8  系统F片断
 23.9  参数性
 23.10不可预言性
 23.11注释
 第24章  存在类型
 24.1  引言
 24.2  带存在量词的数据抽象
 24.3  存在量词编码
 24.4  注释
 第25章  系统F的ML实现
 25.1  类型的无名表示
 25.2  类型移位和代换
 25.3  项
 25.4  求值
 25.5  类型化
 第26章  囿量词
 26.1  引言
 26.2  定义
 26.3  实例
 26.4  安全
 26.5  囿存在量词类型
 26.6  注释
 第27章  实例分析:命令性对象,约式
 第28章  囿量词的元理论
 28.1  揭示
 28.2  最小化类型
 28.3  核心F<∶系统的子类型化
 28.4  全F<∶系统中的子类型化
 28.5  全F<∶系统的不可判定性
 28.6  合类型和交类型
 28.7  囿存在量词
 28.8  囿量词和最小类型
 第六部分  高 阶 系 统
 第29章  类型算子和分类
 29.1  直觉
 29.2  定义
 第30章  高阶多态
 30.1  定义
 30.2  实例
 30.3  性质
 30.4  Fω系统片断
 30.5  进一步讨论:依赖类型
 第31章  高阶子类型化
 31.1  直觉
 31.2  定义
 31.3  性质
 31.4  注释
 第32章  实例学习:纯函数对象
 32.1  简单对象
 32.2  子类型化
 32.3  囿量词
 32.4  接口类型
 32.5  向对象发送消息
 32.6  简单的类
 32.7  多态更新
 32.8  添加实例变量
 32.9  含self的类
 32.10注释
 附录A  部分习题解答
 附录B  标记约定
 参考文献
</font>