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

目　　录

第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 等式、可靠性和完备性