在最广泛的层面上，类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上，它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的，并在伯特兰·罗素和 Alfred North Whitehead 的《数学原理》中起到重要作用。
在计算机科学分支中的编程语言理论中，类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型 lambda 演算的研究。
简单的类型论
罗素公理体系
直觉类型论
有类型 lambda 演算
类型系统
域理论
范畴论
进一步阅读
Stanford Encyclopedia of Philosophy: Type Theory" -- by Thierry Coquand.
National Institute of Standards and Technology: Abstract data type
A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references. Pages 3-4 appear relevant. Reference number [6] looks good, but it may not be available online.
Constable, Robert L., 2002, "Naïve Computational Type Theory," in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213-259.
The Nuprl Book: "Introduction to Type Theory."
