有类型λ演算

有类型lambda演算是使用lambda符号（）指示匿名函数抽象的一种有类型的形式化。有类型lambda演算是基础编程语言并且是有类型的函数式编程语言如ML和Haskell和更间接的指令式编程语言的基础。它们通过Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型lambda演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型lambda演算被看作无类型lambda演算的精细化。更现代的观点把有类型lambda演算看做更基础的理论，而把无类型lambda演算看作它的只有一个类型的特殊情况。