Az intuicionista típuselmélet (más néven Martin-Löf elmélet vagy konstruktív típuselmélet ) egy Per Martin-Löf svéd matematikus és filozófus által 1972-ben publikált típuselmélet. Az elmélet célja a konstruktív matematika formalizálása volt , amelynek konstruktív objektumai Markov Jr. szerint "egyes figurák, amelyek elemi konstruktív objektumokból állnak" [1] . Ebben az irányban a matematika logikája a matematikafilozófia részének tekinthető , amelyben használják [2] .
Az intuicionista típuselméletnek több változata is létezik. Martin-Löf maga javasolta az elmélet intenzionális és extenzionális változatát. Kezdetben nem predikatív változatokat is bemutattak, ami nem volt összhangban Girard paradoxonával . Azonban minden verzió megtartja a függő típusokat használó konstruktív logika alapvető stílusát .