直觉类型论、或构造类型论、或Martin-Löf 类型论、或就叫类型论是基于数学构造主义的函数式编程语言、逻辑和集合论。直觉类型论由瑞典数学家和哲学家 Per Martin-Löf 在1972年提出的。 Martin-Löf 已经多次修改了它的提议；先是非直谓性的而后是直谓性的，先是外延的而后是内涵的类型论变体。

构造类型论为计算机科学家提供了一个框架，以一种优雅和灵活的方式把逻辑和程序设计语言结合起来：在同一形式系统中，可以同时表达规约和（函数式语言）程序，从证明规则可以导出正确的程序，并验证程序具有某种性质，从而在同一系统内完成程序的开发和验证。构造类型论的三大理论基石是：直觉类型论和构造数学、弄演算和函数式语言程序设计与实现、证明论和Curry-Howard同态。直觉类型论为构造数学提供直觉解释。它是一个逻辑框架，可表达和解释其它逻辑或理论。从它的规范化证明立即得出其所表达理论的规范化。直觉类型论基于的是命题和类型的同一: 一个命题同一于它的证明的类型。这种同一通常叫做Curry-Howard同构，它最初公式化了命题逻辑和简单类型 lambda演算。类型论通过介入包含着值的依赖类型把这种同一扩展到谓词逻辑。类型论内在化了 Brouwer、Heyting 和 Kolmogorov 提议的叫做 BHK释义的直觉逻辑释义。类型论的类型扮演了类似于集合在集合论的角色，但是在类型论中的函数总是可计算的。

在直觉类型论的上下文中，连结词是可能使用已给定的类型而构造类型的一种方式。类型论的基本连结词有：

-类型

-类型，也叫做依赖函数类型，一般化了普通的函数空间，建模其结果的类型可以随它们的输入而变化的函数，比如，对实数的 -元组写为 ，则 表示对给定的自然数返回这个大小的实数元组的函数的类型。在值域类型实际上不依赖于输入的时候，普通函数空间作为特殊情况出现，比如 是从自然数到实数的函数的类型，它也写为 。使用 Curry-Howard同构，-类型还充当建模蕴涵和全称量化：比如，居留于 的一个项，它对任何一对自然数的函数指派加法对这个数对是交换性的证明，并因此可以被当作加法对于所有自然数是交换性的一个证明。

-类型

-类型，也叫做依赖乘积类型，一般化了普通的笛卡尔积，建模第二个构件的类型依赖于第一个构件的有序对，比如类型 表示自然数和这个大小的实数的元组的有序对的类型，就是说，这个类型可以用来建模任意长度的序列(通常叫做列表)。在第二个构件的类型实际上不依赖于第一个构件的时候，常规的笛卡尔积类型作为特殊情况出现，比如 是自然数和实数的有序对的类型，它也写为 。再次使用 Curry-Howard同构，-类型也充当建模合取和存在量化。

有限类型

特别重要的是 (空类型)、 (单位类型)和 (布尔值或真值)。再次用到 Curry-Howard同构， 表示假而 表示真。使用有限类型，我们可以定义否定为 ，服从Curry-Howard同构，不相交并集也表示析取，它可以定义为 。

等式类型

给定 ，则 是 等于 的等式证明。只有一个(规范的) 的居留，并且这是自反性 的证明。

归纳类型

归纳类型的基本例子是自然数 的类型，它是通过和生成的。命题为类型原理的一个重要应用是通过对用索引的给定类型的一个消除常量：来把(依赖的)原始递归和归纳同一起来的。在一般的归纳类型中可以被定义为 W-类型，它是良基的树的类型。

一类重要的归纳类型是像上面提及的向量的归纳类型家族，它们是归纳生成自构造子 和 。再次用到Curry-Howard同构，归纳类型家族对应于归纳定义的关系。

全集

全集的一个例子是，它是所有小类型的全集，它包含前面介绍的所有类型的名字。对于每个名字 我们关联上一个类型，这是它的外延或意义。标准上是假定全集的一个直谓性等级: 对于每个自然数，这里的全集包含以前的全集的一个代码，就是说，我们通过而有。这个等级经常被假定为是累积性的，就是说来自的代码被嵌入了。已经研究了更强的全集原理，比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了构造演算，它是带有非直谓性全集的类型论，从而把类型论同 Girard 的系统F 合并起来了。这个扩展不被直觉主义者所普遍接受，因为它允许非直谓性的，就是循环的构造，这经常用经典推理来识别。

一个基本区别是外延和内涵的类型论。在外延类型论中定义性(就是计算性)等式不区别于需要证明的命题性等式。作为结论类型检查成为不可判定性的。相反的，在内涵类型论中，类型检查是可判定性的，但是很多数学概念的表达是不标准的，因为缺乏外延推理。这是对这种折中是否是不可避免的和在内涵类型论中缺乏外延原理是一个特色还是一个缺陷的讨论的一个主题。