Інтуїціоні́стська тео́рія ти́пів (також відома як теорія Мартіна-Льофа або конструктивна теорія типів) — теорія типів, яку розробив шведський математик і філософ Пер Мартін-Льоф, опублікована в 1972 року. Метою теорії послужила формалізація конструктивної математики, конструктивні об'єкти якої, згідно з Марковим-молодшим, є «деякими фігурами, складеними з елементарних конструктивних об'єктів». У цьому напрямі логіку математики можна розглядати як частину філософії математики, у складі якої використовується.

Є кілька версій інтуїціоністської теорії типів. Сам Мартін-Льоф запропонував як , так і  варіанти теорії. На початку також представлено непредикативні версії, не сумісні з парадоксом Жірара. Проте всі версії зберігають базовий стиль конструктивної логіки з використанням залежних типів.

Примітки





