Intuitionistisk typeteori (også kendt som Martin-Löf-teori eller konstruktiv typeteori ) er en typeteori udviklet af den svenske matematiker og filosof Per Martin-Löf , udgivet i 1972. Målet med teorien var formaliseringen af konstruktiv matematik , hvis konstruktive objekter ifølge Markov Jr. er "nogle figurer sammensat af elementære konstruktive objekter" [1] . I denne retning kan matematikkens logik betragtes som en del af matematikkens filosofi , hvori den bruges [2] .
Der er flere versioner af intuitionistisk typeteori. Martin-Löf foreslog selv både intensional og extensional versioner af teorien. I begyndelsen blev der også præsenteret ikke-prædikative versioner, i modstrid med Girards paradoks . Imidlertid bevarer alle versioner den grundlæggende stil af konstruktiv logik ved hjælp af afhængige typer .