有類型λ演算

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

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

種類

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

某些有類型lambda演算介入「子類型」的概念，就是說如果$A$是$B$的子類型，則類型$A$的所有項也有類型$B$。帶有子類型的有類型lambda演算是帶有合取類型和$F^{\leq }$（F-sub）的簡單類型lambda演算。

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

應用

有類型lambda演算在為程式語言設計新型別系統的時候扮演了關鍵性角色；這裏類型能力通常擷取了程式想要的性質，比如程式不會導致主記憶體訪問違規。

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

參見

• 簡單類型lambda演算
• 系統F
• 邏輯框架
• 構造演算
• 直覺類型論