Tüübiteooria
Tüübiteooria on mõne üksiku tüübisüsteemi formaalne esitus ja tüübisüsteemide uurimise valdkond matemaatikas ja informaatikas. Mõned tüübiteooriad pakuvad hulgateooria kõrval alternatiivset alust matemaatikale. Kaks tüübiteooriat, mida on pakutud matemaatika alusteooriateks on Alonzo Churchi tüübitud lambda-arvutus ning Per Martin-Löfi intuitsionistlik tüübiteooria. Enamik arvutipõhiseid tõestusassistente on rajatud mõnele tüübiteooriale.