形式陈述

在直觉主义逻辑与类型 λ 演算之间，蕴含 $A\to B$$A\to B$ 对应函数类型，合取对应积类型，析取对应和类型；一个命题的证明对应其类型的一个项。β-归约对应自然演绎中的正规化或迂回消去；在序列演算中，与之密切对应的是 cut elimination，但两者不应在未指定证明系统时直接视为同一条规则。

直觉

写出一个类型正确的程序，就是构造了相应命题的证据；运行程序则规范化这份证据。

例子与边界

类型 $A\to A$$A\to A$ 的项 $\lambda x.x$$\lambda x.x$ 对应命题 $A\Rightarrow A$$A\Rightarrow A$ 的证明。经典逻辑需要控制算子、双重否定等额外结构，不能与最简单的纯函数类型直接等同。

推论与应用

该对应支撑 Coq、Agda、Lean 等证明助理，以及依赖类型程序设计和 proof-carrying code。

参考资料

• William A. Howard, “The Formulae-as-Types Notion of Construction,” 1980.
• Morten Heine Sørensen and Paweł Urzyczyn, Lectures on the Curry–Howard Isomorphism.