来自 Classic Papers in Programming Languages and Logic
个人相比科研更喜欢纯粹的阅读（狗头），也感觉需要空闲时间探索一下经典论文，让 Gemini 帮我生成了一个阅读计划，最好能读下来：
| 建议日期 | 主题单元 | 阅读论文 | 核心要点与建议 | 完成 |
|---|---|---|---|---|
| 第一单元 | 计算的基石：Lambda演算与函数式编程 | |||
| 2025-12-08 (一) | 1.1 Lambda 演算 | Church & Rosser - Some Properties of Conversion | 起点。 理解计算的最纯粹形式。重点关注β-归约 (规则II)，这是所有函数调用的理论模型。 | [ ] |
| 2025-12-10 (三) | 1.2 理论到实践 | McCarthy - Recursive Functions of Symbolic Expressions | 从纯理论到第一个伟大的函数式语言 LISP。思考 eval 函数如何体现了计算的本质。 |
[ ] |
| 2025-12-15 (一) | 1.3 计算的机械化 | Landin - The Mechanical Evaluation of Expressions | 函数式语言是如何在机器上运行的？SECD 机的设计是理解解释器和虚拟机的经典模型。 | [ ] |
| 2025-12-17 (三) | 1.4 语言设计的哲学 | Landin - The Next 700 Programming Languages | 一篇充满远见的宣言。核心思想：大多数语言只是一个优雅核心 (ISWIM) 配上不同的“语法糖”。 | [ ] |
| 第二单元 | 程序的正确性：逻辑与验证 | |||
| 2025-12-22 (一) | 2.1 公理语义 | Hoare - An Axiomatic Basis for Computer Programming | 引入著名的“霍尔逻辑” {P} C {Q}。这是思考和证明程序正确性的基石。 |
[ ] |
| 2025-12-24 ~ 2026-01-04 | 🎄 年末假期 🎄 | 休息、回顾或自由探索 | 圣诞及新年假期。 暂停新内容的学习，可以花点时间回顾第一单元，确保基础牢固。 | - |
| 2026-01-05 (一) | 2.2 程序推导 | Dijkstra - Guarded Commands... | 从“验证”程序到“推导”程序。Dijkstra 的思想是让程序和它的证明一同被构造出来。 | [ ] |
| 2026-01-07 (三) | 2.3 并发模型 | Hoare - Communicating Sequential Processes | 将逻辑思想扩展到并发世界。CSP 是 Go 等现代语言并发模型的理论源头。 | [ ] |
| 第三单元 | 程序的意义：语义学 | |||
| 2026-01-12 (一) | 3.1 操作语义 | Plotkin - A Structural Approach to Operational Semantics | 篇幅很长，分两次。 (第一部分) 学习定义程序“如何一步步执行”的现代标准方法。 | [ ] |
| 2026-01-14 (三) | 3.1 操作语义 | Plotkin - A Structural Approach to Operational Semantics | (第二部分) 继续阅读 Plotkin，重点理解 SOS (Structured Operational Semantics) 的优雅之处。 | [ ] |
| 2026-01-19 (一) | 3.2 指称语义 | Scott & Strachey - Towards a Mathematical Semantics... | 另一种视角：程序“计算出什么”。它将程序映射为数学对象，是进行抽象推理的强大工具。 | [ ] |
| 2026-01-21 (三) | 3.3 解释器与高阶 | Reynolds - Definitional Interpreters for Higher-Order... | 用语言自身来定义语言。这篇论文深刻地揭示了高阶函数、作用域和“续延 (Continuation)”的奥秘。 | [ ] |
| 第四单元 | 类型与逻辑的对偶：证明论与类型论 | |||
| 2026-01-26 (一) | 4.1 逻辑的结构 | Gentzen - Investigations into Logical Deduction | 回到逻辑的源头。理解“自然演绎”是理解后续所有“命题即类型”思想的前提。 | [ ] |
| 2026-01-28 (三) | 4.2 革命性洞见 | Howard - The Formulae-as-Types Notion of Construction | “柯里-霍华德同构”的核心文献。程序即证明，类型即命题。这是本课程最深刻的思想之一。 | [ ] |
| 2026-02-02 (一) | 4.3 构造性理论 | Martin-Löf - On the Meanings of the Logical Constants... | 将柯里-霍华德同构发展成一个完备的系统——直觉主义类型论。现代证明助理 (Coq, Agda) 的理论基础。 | [ ] |
| 2026-02-04 (三) | 4.4 新的逻辑 | Girard - Linear Logic | 篇幅很长，建议先通读。 引入“资源敏感”的线性逻辑。它对状态、并发和优化的建模有深远影响。 | [ ] |
| 第五单元 | 抽象的力量：类型系统与模块化 | |||
| 2026-02-09 (一) | 5.1 泛型与多态 | Reynolds - Toward a Theory of Type Structure | 泛型（Generics）的理论基础——System F。理解它如何让代码在保持类型安全的同时变得更通用。 | [ ] |
| 2026-02-11 (三) | 5.2 类型自动推导 | Damas & Milner - Principal Type-Schemes for Functional Programs | Haskell/ML 等语言的“魔法”背后：著名的 Hindley-Milner 类型推导算法。 | [ ] |
| 2026-02-16 (一) | 5.3 抽象的边界 | Reynolds - Types, Abstraction, and Parametric Polymorphism | 多态带来的“免费定理”。它告诉我们，类型签名本身就极大地约束了函数的行为。 | [ ] |
| 2026-02-18 (三) | 5.4 模块与存在 | Mitchell & Plotkin - Abstract Types have Existential Types | 模块化和信息隐藏的类型论基础。抽象数据类型ADT原来就是“存在类型”。 | [ ] |
| 2026-02-23 (一) | 5.5 高级模块化 | MacQueen - Using Dependent Types to Express Modular Structure | ML 语言模块系统的基石。展示了如何用更强大的类型（依赖类型）来构建灵活的模块。 | [ ] |
| 2026-02-25 (三) | 5.6 模块与阶段 | Harper, Mitchell, Moggi - Higher-Order Modules... | 进一步发展了 ML 模块系统，并澄清了编译时（静态）和运行时（动态）的重要区别。 | [ ] |
| 第六单元 | 计算的结构：Monad、控制流与风格 | |||
| 2026-03-02 (一) | 6.1 副作用的统一 | Moggi - Computational Lambda-calculus and Monads | 里程碑论文。 Moggi 首次提出用 Monad 来统一建模各种计算副作用（IO、状态、异常等）。 | [ ] |
| 2026-03-04 (三) | 6.2 风格的解放 | Backus - Can Programming Be Liberated from the von Neumann Style? | 图灵奖演讲。一篇充满激情的宣言，倡导函数式编程，批判传统命令式编程的弊病。 | [ ] |
| 2026-03-09 (一) | 6.3 经典逻辑的计算 | Murthy - An Evaluation Semantics for Classical Proofs | 将程序与证明的联系从直觉主义逻辑扩展到经典逻辑，揭示了与 call/cc 等控制流操作的深刻关联。 |
[ ] |
| 2026-03-11 (三) | 总结与回顾 | 恭喜完成！ 花时间重新审视所有论文，看看它们是如何交织在一起，共同塑造了现代编程语言和计算机科学的。 | - |