类型理论：一种用“类型（type）”来分类表达式、限制可进行的运算、并为数学与计算机程序提供形式化基础的理论框架。常用于编程语言类型系统、逻辑与证明、以及形式化验证等领域。（也可指多种具体体系的统称，如简单类型λ演算、依赖类型理论等。）
/taɪp ˈθɪəri/
Type theory helps prevent certain programming errors.
类型理论有助于防止某些编程错误。
In modern proof assistants, type theory can serve as a foundation where programs and proofs are expressed in the same formal language.
在现代证明助手中，类型理论可以作为基础，使程序与证明用同一种形式语言来表达。
“type”源自希腊语 typos，原意与“印记、模子、范型”相关，引申为“类别、类型”；“theory”源自希腊语 theōria，意为“观察、思辨”，后发展为“理论”。合在一起，“type theory”字面即“关于类型的理论”，在20世纪逻辑学与计算理论发展中逐渐成为关键术语。
Select Language