Інтуїціоні́стська тео́рія ти́пів (також відома як теорія Мартіна-Льофа або конструктивна теорія типів) — теорія типів, яку розробив шведський математик і філософ Пер Мартін-Льоф, опублікована в 1972 року. Метою теорії послужила формалізація конструктивної математики, конструктивні об'єкти якої, згідно з Марковим-молодшим, є «деякими фігурами, складеними з елементарних конструктивних об'єктів»Марков А. А. О конструктивной математике. Проблемы конструктивного направления в математике. 2.Конструктивный математический анализ, Сборник работ. Тр. МИАН СССР, 67, Изд-во АН СССР. У цьому напрямі логіку математики можна розглядати як частину філософії математики, у складі якої використовуєтьсяД. Д. Рогозин; А. В. Родин. Теория типов в логике и основаниях математике. Москва, Институт философии РАН. 2016.
Є кілька версій інтуїціоністської теорії типів. Сам Мартін-Льоф запропонував як , так і варіанти теорії. На початку також представлено непредикативні версії, не сумісні з парадоксом Жірара. Проте всі версії зберігають базовий стиль конструктивної логіки з використанням залежних типів.
Примітки