编程语言理论入门

编程语言理论（PLT）是计算机科学的一个偏理论的分支，涉及称为编程语言的形式语言的设计、实现、分析、表征和分类。编程语言理论与其他领域密切相关，包括数学、软件工程和语言学。最好具备一定的抽象代数和形式逻辑的基础，比如经典逻辑。
- 一般来说「离散数学」课程教授的抽象代数内容已经足够，但是随着研究深入你可以也会遇到非常难懂的代数内容，所以在此我也推荐几本抽象代数的书籍：
  - A Computational Introduction to Number Theory and Algebra — Victor Shoup
  - Advanced Modern Algebra — Joseph J. Rotman [pdf](http://www.math.hcmuns.edu.vn/~nvdong/DaiSoDaiCuong/Advanced Modern Algebra - Joseph J. Rotman.pdf)
  - A Survey of Modern Algebra — Birkhoff and MacLane Scribd
- 还有一些数学思想、证明技巧的书籍
  - Introduction to Mathematical Thinking — Keith Devlin
  - How to prove it — Daniel J. Velleman
学习编程语言理论可能是一个艰难的旅程，即使对于高水平的程序员来说，这也可能是无比困难的一件事。此资源尽力为你提供帮助，祝你好运！

CS242 Programming Languages

所属大学：Stanford
编程语言：OCaml, Rust
指导思想：From Theory to Systems: A Grounded Approach to Programming Language Education

CS242是一门讲程序语言 (Programming Language, PL) 的课程，但不是传统意义上的纯理论导向。这门课程首先介绍了如 Lambda 演算，类型系统这样的经典 PL 理论，然后借助系统编程的思想和实际的编程语言来驱动学生理解这些理论，展示了它们是如何在实际编程中帮助开发者避免各种错误。

前面几次的作业偏 PL 理论，如果你觉得前面几次的课程内容和作业过于理论，可以重点尝试使用 OCaml 实现解释器的作业，它既能让你对之前的理论有更深刻的理解，又能让你实战一个函数式语言的类型检查和解释。而后面的作业则更倾向于利用理论来指导系统编程与设计，尤其是 Rust 和它独特的所有权机制与类型系统。虽然我们要经常与编译器搏斗，但这也恰好说明了类型系统和理论对于编程和设计的意义。

编程语言设计原理

所属大学：北京大学
编程语言：OCaml

程序语言理论与实现

所属机构：粤港澳大湾区数字经济研究院（IDEA）
编程语言：ReScript

本课程主要讲授程序语言设计与实现中的理论和实践，相较传统编译原理课程花费比较多的篇幅在词法分析、语法分析、语法树构造等章节，这门课程会直接从 Lambda 演算切入介绍编程语言最核心的部分，但和国外的同类课程不同的是，更多的注重把理论和实践相结合。该课程主要面向对基础软件感兴趣的学生、及从事软件研发的业界同行等，几乎没有前置条件，完成本课程后学生可以完成一个自己的简单编译器。

笔者注：授课的示例代码使用 ReScript 语言，起源于授课老师张宏波的个人作品，也是迄今国内第一个在国际范围内有一定影响力的通用编程语言。张老师在国内的PL基础教育也是花费了很多心思，笔者之前有幸在 IDEA 实习过一段时间，也得到了张老师很多指导。最近我们也是开展了一个程序语言理论与实现的进阶课程，教你用 MoonBit 语言（张老师带领的团队设计的新编程语言）实现一个 mini-moonbit 编译器，并且举办了相关比赛（奖金丰厚，感兴趣的同学可以联系笔者）。

编程语言理论入门 ​

CS242 Programming Languages ​

编程语言设计原理 ​

程序语言理论与实现 ​

推荐书籍 / 博客 / 论文 ​

编程语言理论入门

CS242 Programming Languages

编程语言设计原理

程序语言理论与实现

推荐书籍 / 博客 / 论文