Intuitionistinen tyyppiteoria (tunnetaan myös nimellä Martin-Löf-teoria tai konstruktiivinen tyyppiteoria ) on ruotsalaisen matemaatikon ja filosofin Per Martin-Löfin vuonna 1972 kehittämä tyyppiteoria . Teorian tavoitteena oli konstruktiivisen matematiikan formalisointi , jonka konstruktiiviset objektit ovat Markov Jr.:n mukaan "joitakin hahmoja, jotka koostuvat alkeellisista konstruktiivisista objekteista" [1] . Tässä suunnassa matematiikan logiikkaa voidaan pitää osana matematiikan filosofiaa , jossa sitä käytetään [2] .
Intuitionistisesta tyyppiteoriasta on olemassa useita versioita. Martin-Löf itse ehdotti teoriasta sekä intensiaalista ja ekstensiaalista versiota. Alussa esitettiin myös ei-predikatiivisia versioita, mikä oli ristiriidassa Girardin paradoksien kanssa . Kaikki versiot säilyttävät kuitenkin rakentavan logiikan perustyylin käyttämällä riippuvaisia tyyppejä .