直觉类型论、或构造类型论、或Martin-Löf 类型论、或就叫类型论是基于数学构造主义的函数式编程语言、逻辑和集合论。直觉类型论由瑞典数学家和哲学家 Per Martin-Löf 在1972年提出的。 Martin-Löf 已经多次修改了它的提议；先是非直谓性的而后是直谓性的，先是外延的而后是内涵的类型论变体。构造类型论为计算机科学家提供了一个框架，以一种优雅和灵活的方式把逻辑和程序设计语言结合起来：在同一形式系统中，可以同时表达规约和（函数式语言）程序，从证明规则可以导出正确的程序，并验证程序具有某种性质，从而在同一系统内完成程序的开发和验证。构造类型论的三大理论基石是：直觉类型论和构造数学、弄演算和函数式语言程序设计与实现、证明论和Curry-Howard同态。直觉类型论为构造数学提供直觉解释。它是一个逻辑框架，可表达和解释其它逻辑或理论。从它的规范化证明立即得出其所表达理论的规范化。直觉类型论基于的是命题和类型的同一: 一个命题同一于它的证明的类型。这种同一通常叫做Curry-Howard同构，它最初公式化了命题逻辑和简单类型 lambda演算。