Интуиционистская теория типов (теория типов Мартин-Лёфа, конструктивная теория типов) — теория типов, созданная Пером Мартин-Лёфом в 1972 году с целью формализации конструктивной математики, объекты которой, согласно Маркову-младшему, являются «некоторыми фигурами, составленными из элементарных конструктивных объектов»[1]. В данном направлении логика математики может рассматриваться как часть философии математики, в составе которой и используется[2].
Имеются несколько вариантов теории: Мартин-Лёфом предложены как интенсиональный[англ.], так и экстенсиональный[англ.] варианты, также были разработаны непредикативные версии, несовместимые с парадоксом Жирара. Тем не менее, все варианты сохраняют базовый стиль конструктивной логики с использованием зависимых типов.