在數學、邏輯學和計算機科學中，類型理論是對特定類型系統的正式表述，一般來說，類型理論是對類型系統的學術研究。一些類型理論作為集合理論的替代品，作為數學的基礎。兩個被提議作為基礎的有影響力的類型理論是AlonzoChurch的類型化λ-微積分和PerMartin-L?f的直覺類型理論。大多數計算機化的證明書寫系統都使用類型理論作為其基礎。一個常見的是ThierryCoquand的歸納構造微積分（CalculusofInductiveConstructions）。

類型理論是為了避免在基于天真的集合論和形式邏輯的數學基礎上出現悖論而創建的。羅素悖論是由伯特蘭-羅素發現的，它的存在是因為一個集合可以用所有可能的集合來定義，其中包括它自己。1902年至1908年期間，伯特蘭-羅素提出了各種類型的理論來解決這個問題。到了1908年，羅素得出了一個夯實的類型理論，以及一個可還原性公理，這兩者在懷特海和羅素的《數學原理》中都有突出的表現，在1910年至1913年期間出版。這個系統避免了羅素的悖論，它建立了一個類型的層次結構，然后把每個具體的數學實體分配給一個類型。一個給定類型的實體完全由該類型的子類型建立，從而防止一個實體被定義為使用其本身。羅素的類型理論排除了一個集合是自身成員的可能性。類型并不總是在邏輯中使用。還有其他技術來避免羅素的悖論。當與一個特定的邏輯，即AlonzoChurch的lambdacalculus一起使用時，類型確實得到了支持。

最著名的早期例子是丘奇的簡單類型的λ微積分。Church的類型理論幫助形式化系統避免了困擾最初的無類型λ微積分的Kleene-Rosser悖論。Church證明了它可以作為數學的基礎，它被稱為高階邏輯。現在，類型理論這個短語一般指的是圍繞λ微積分的類型系統。一個有影響力的系統是PerMartin-L?f的直覺類型理論，它被提議作為構造數學的基礎。另一個是ThierryCoquand的構造微積分，它被Coq、Lean和其他證明助手（計算機化的證明書寫程序）作為基礎。類型理論是一個活躍的研究領域，正如同構類型理論所證明的那樣。

有很多類型理論，這使得我們很難產生一個全面的分類法；本文并不是一個詳盡的分類法。下面是對那些不熟悉類型理論的人的介紹，包括一些主要的方法。

在類型理論中，每個術語都有一個類型。一個術語和它的類型通常被寫成術語：類型。在類型理論中，一個常見的類型是自然數，通常寫成或nat。另一個是布爾邏輯值。因此，一些非常簡單的術語及其類型是。0+0:nat2+3:nat1+(1+(1+0)):nat術語也可以包含變量。

變量總是有一個類型。因此，假設x和y是nat類型的變量，以下也是有效的術語。x:natx+2:natx+(x+y):nat除了nat和bool，還有更多類型。我們已經看到了術語add，它不是一個nat，而是一個函數，當應用于兩個nat時，計算出一個nat。add的類型將在后面介紹。首先，我們需要描述計算到。計算類型理論有一個內置的計算符號。下面的術語都是不同的。1+4:nat3+2:nat0+5:nat，但它們都計算到了5:nat這個術語。在類型理論中，我們用reduction和reduce來指代計算。