简单类型 λ 演算

$A\to B$ 是函数接口：输入须有 $A$ 型，应用结果获得 $B$ 型。推导树把每次变量使用、抽象和应用的接口匹配记录下来；执行前无法构造推导的项被静态排除。

简单类型没有解递归类型方程的机制。给 $xx$ 定型会要求 $x$ 既有某个参数类型 $A$，又有函数类型 $A\to B$，进而需要有限类型满足 $A=A\to B$。这个方程无解，因而循环项 $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$ 被挡在类型推导之外。

恒等项可由

定型。若上下文含 $f:A\to B$ 与 $x:A$，应用规则得到 $fx:B$，连续两次抽象便有

这棵推导同时展示箭头右结合与上下文中临时假设的解除。

类型判断不等于运行结果。开项 $x:A⊢x:A$ 良类型，却在没有环境时不能独立执行；闭项 $(\lambda x:A.x)(\lambda y:B.y)$ 是否良类型取决于实参类型是否正好是 $A$。原始语法相似不能替代推导。

加入固定点常量 $\mathsf{fix}:(T\to T)\to T$ 后，可以写出良类型发散项；进展与保持仍可能成立，强正规化却立即失效。类型安全与终止是不同元定理。

STLC 是静态语义与动态语义相互作用的最小实验场。进展与保持定理公理库进展与保持定理Progress and preservation · Type safety在固定动态语义下，良类型闭项可继续或已是结果，且每一步都保持其类型。说明良类型闭项不会因类型错误卡住，强正规化定理公理库简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。另外证明每条完整 β-归约路径都有限。后者严格强于某个求值策略终止。

在Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，箭头类型对应蕴含，项对应自然演绎证明，β-归约对应证明化简。积、和、多态与依赖类型可继续扩展这条对应，但每项扩展都需重新检查类型规则、动态规则与元定理。