Інтуїціоністська теорія типів

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

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