\t本书是关于现代类型论的专著。与集合论类似，现代类型论是数学及诸多领域的
基础语言。本书介绍了现代类型论(及其元理论)，并以自然语言语义学和计算机辅助
推理为例对以现代类型论为基础的应用领域进行深入浅出的讨论。作为基础语言，现
代类型论一方面提供了丰富的描述机制，另一方面便于理解与实现，因此与集合论相
比有着多方面的优势。这些优点在实际运用中展示出来：作为范例，书中深入研究了
基于现代类型论的自然语言语义学，以加深读者对此的理解。书中还介绍了以现代类
型论为基础的交互式证明技术在数学形式化、计算机程序验证及自然语言推理诸方面
的应用，进一步展示了使用现代类型论作为基础语言的优势。



\t本书适合研究自然语言语义学、计算机科学和逻辑学等领域的学者及研究生和
对相关内容感兴趣的读者。

第1章现代类型论及其应用1
1.1简单类型论与现代类型论发展概述1
1.2现代类型论概论及特点综述4
1.2.1基本概念概述4
1.2.2现代类型论的特点及其与其他形式系统的区别6
1.3现代类型论的若干应用和本书概述9
第2章现代类型论12
2.1判断、上下文及定义性等式12
2.2类型构造算子15
2.2.1函数的依赖类型（Π类型）15
2.2.2序对的依赖类型（Σ类型）17
2.2.3不相交并类型20
2.2.4有穷类型21
2.3归纳、递归及计算理论22
2.3.1自然数类型22
2.3.2列表类型和向量类型24
2.4类型空间27
2.4.1Prop：逻辑命题的非直谓类型空间27
2.4.2直谓类型空间及其描述方式29
2.4.3类型空间应用举例33
……