编程语言与类型系统

这条精选路线把三个常被分开讲的能力连起来：程序怎样表示计算、类型怎样被推断、我们怎样描述程序是否满足预期。

适合用过类型语言，想理解原理

建议顺序计算模型 → 类型推断 → 正确性

读法手算最小例子

目标理解语言工具的保证边界

先读这 3 篇

论文Pillar计算模型

Lambda Calculus

用变量、函数和应用三个核心元素理解“计算”可以怎样被表达。

先获得最小计算模型，后面的类型规则才有落点。

论文Pillar类型推断

Hindley-Milner

理解编译器如何在少写类型标注时仍推导出通用类型。

把统一、泛化和实例化连成一条推断流程。

论文程序逻辑正确性

Hoare Logic

用前置条件、程序和后置条件描述“这段程序做对了什么”。

类型能排除一部分错误，但程序正确性需要更明确的规格。

读完你应该能回答

1. Lambda Calculus 为什么只靠函数也能表达计算？
2. Hindley-Milner 的类型推断与运行时类型检查有什么差别？
3. 一个类型正确的程序为什么仍可能不满足业务要求？
4. Hoare triple 中前置条件和后置条件分别承担什么责任？

这页只提供学习主线。更多论文可进入 论文精选队列；需要按名称查找时再用 论文全景索引。