有類型λ演算

有類型lambda演算是使用lambda符號指示匿名函數抽象的一種有類型的形式化。有類型lambda演算是基礎編程語言並且是有類型的函數式編程語言如ML和Haskell和更間接的指令式編程語言的基礎。它們通過Curry-Howard同構密切關聯於直覺邏輯並可以被認為是範疇的類的內部語言，比如簡單類型lambda演算是笛卡兒閉範疇（CCC）的語言。

傳統上，有類型lambda演算被看作無類型lambda演算的精細化。更現代的觀點把有類型lambda演算看做更基礎的理論，而把無類型lambda演算看作它的只有一個類型的特殊情況。 ^[1] 

已經研究了各種有類型lambda演算。簡單類型lambda演算的類型只是基本類型（或類型變量）和函數類型。系統T向簡單類型lambda演算擴展了自然數類型和更高階的原始遞歸函數；在這個系統中在可證明在皮亞諾算術中是遞歸函數的所有函數都是可定義的。系統F通過在所有類型上的全稱量化允許多態性；從邏輯的觀點看它可以描述可證明在二階邏輯中是全函數的所有函數。有依賴類型的lambda演算是直覺類型論，構造演算和邏輯框架（LF）的基礎，它是帶有依賴類型的純lambda演算。基於Berardi的工作，Barendregt提議了Lambda立方體來系統化純有類型lambda演算（包括簡單類型lambda演算，系統F，LF和構造演算）之間的關係。

某些有類型lambda演算介入“子類型”的概念，就是説如果A是B的子類型，則類型A的所有項也有類型B。帶有子類型的有類型lambda演算是帶有合取類型的簡單類型lambda演算。

迄今提到的所有西，除了無類型lambda演算是例外，都是“強規範化”的：所有計算都會終止。結論是他們作為邏輯都是自恰的，就是説這裏有無居留（uninhabited）類型。但是存在着不是強規範化的有類型lambda演算。比如帶有所有類型的一個類型（Type:Type）的依賴類型lambda演算由於Girard悖論而不是強規範化的。這個系統也是最簡單的純類型系統，它是推廣Lambda立方體的一種形式化。有明確的遞歸組合子的系統，比如GordonPlotkin的PCF，不是規範化的，但是它們不意圖被解釋為邏輯。實際上，PCF（可計算函數的編程語言）是元典型（prototypical）的有類型的函數式編程語言，這裏的類型被用來確保程序是有良好行為的而不必須是終止的。 ^[1] 

有類型lambda演算在為編程語言設計新類型系統的時候扮演了關鍵性角色；這裏類型能力通常捕獲了程序想要的性質，比如程序不會導致內存訪問違規。

在編程中，強類型編程語言的例程（函數，過程，方法）密切關聯於有類型lambda表達式。Eiffel有一個“內線代理”概念，使得有可能直接定義和操縱有類型lambda表達式，通過這種表達式如agent(p:PERSON):STRINGdoResult:=p.spouse.nameend，指示表示返回一個人配偶的名字的一個函數的一個對象。 ^[1]