Curry-Howard同构
Curry-Howard 对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做 Curry-Howard 同构或公式为类型对应。已经采用了一些不同的公式化，它的原理现在被认为是由美国数学家 Haskell Curry 和逻辑学家 William Alvin Howard 独立发现的。
对应可以在两个层面上看到，首先是类比层次，它声称一个函数计算出的值的类型的断言类比于一个逻辑定理，计算这个值的程序类比于这个定理的证明。在理论计算机科学中，这是连接lambda 演算和类型论的毗邻领域的一个重要的底层原理。它被经常以下列形式陈述为证明是程序。一个可选择的形式化为命题为类型。其次，更加正式的，它指定了在两个数学领域之间的同构，就是以一种特定方式形式化的自然演绎，和简单类型 lambda 演算之间是双射，首先是证明和项，其次是证明归约步骤和 beta 归约。
有多种方式考虑 Curry-Howard 对应。在一个方向上，它工作于编译证明为程序级别上。这里的证明，最初被限定为构造性逻辑 — 典型的是直觉逻辑系统中的证明。而程序是在常规的函数式编程的意义上的；从语法的观点上看，这种程序是用某种 lambda 演算表达的。所以 Curry-Howard 同构的具体实现是详细研究如何把来自直觉逻辑的证明写成 lambda 项。(这是 Howard 的贡献；Curry 贡献了组合子，它是相对于是高级语言的 lambda 演算是能写所有东西的机器语言)。最近，同样处理经典逻辑的 Curry-Howard 对应的扩展可被公式化了，通过对经典有效规则比如双重否定除去和 Peirce 定律关联上明确的用续体比如 call/cc 处理的一类项。
还有一个相反的方向，对一个程序的正确性关联上证明提取的可能性。这在非常丰富的类型论环境中是可行的。实际上理论家对非常丰富类型的函数式编程语言的开发，已经部分的被希望带给 Curry-Howard 对应更加显著的地位的动机所推动。