📄️ 本节路线图
📄️ 目标类型检查器：TAT
名字的由来
📄️ 描写类型系统的工具
元语言和对象语言
📄️ 建立基础定型规则
---
📄️ 无类型λ-演算
现代编程语言的函数，本质上其实是对$\lambda$-演算的一种模仿。自从20世纪30年代Alonzo Church发明了$\lambda$-演算之后，它的简洁、优美、深刻，吸引了无数人。下面是$\lambda$-演算的一个例子，计算两个变量的平方和：
📄️ TAT-STLC的类型系统设计
函数的定型规则: T-Var
📄️ TAT-STLC 的实现
TAT 的类型检查和转译