Intuicionistická teorie typů (také známá jako Martin-Löfova teorie nebo konstruktivní teorie typů ) je teorie typů vyvinutá švédským matematikem a filozofem Perem Martinem-Löfem , publikovaná v roce 1972. Cílem teorie byla formalizace konstruktivní matematiky , jejíž konstruktivní objekty jsou podle Markova mladšího „nějaké figury složené z elementárních konstruktivních objektů“ [1] . V tomto směru lze logiku matematiky považovat za součást filozofie matematiky , ve které se používá [2] .
Existuje několik verzí intuicionistické teorie typů. Martin-Löf sám navrhoval jak intenzionální , tak extenzi verze teorie. Zpočátku byly prezentovány i nepredikativní verze, v rozporu s Girardovým paradoxem . Všechny verze si však zachovávají základní styl konstruktivní logiky pomocí závislých typů .