CS22-编译语言设计与分析

Stanford CS242: Programming Languages

课程简介

所属大学：Stanford
先修要求：对计算机系统和编程语言理论有初步了解
编程语言：OCaml, Rust
课程难度：🌟🌟🌟🌟
预计学时：60 小时

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

主讲老师 Will Crichton 还将他的课程设计思想写成了论文 From Theory to Systems: A Grounded Approach to Programming Language Education，阐述了这条从理论走向系统的教学路线。

我们通过简单介绍每个作业来帮助读者了解这门课程的具体内容：

对 JSON 的形式化与证明
PL 中经典的 Lambda 演算
以 OCaml 为例的函数式编程入门
使用 OCaml 实现一个函数式语言的类型检查器和解释器，同样是 PL 的经典作业
WebAssembly 的理论与实践
Linear Type 和 Rust 的所有权机制
Rust 的异步编程基础
利用 Rust 类型系统设计状态机和实现 session-typed TCP 库
最后的大作业有四个可选项：
1. 使用 Lean 进行定理证明
2. 使用 Rust 实现 Read-Log-Update 同步机制
3. 利用 F* 语言验证文件系统的正确性
4. 在程序语言视角下使用 OCaml 实现一个深度学习框架

这些作业涵盖知识跨度非常大，从最经典的编程语言理论证明和实践到以 Rust 为例的编程语言对于编程和系统设计的影响，再到最后各有特色的大作业。几乎所有的编程作业都有详尽的本地测试，尤其是大作业中的深度学习框架更有超过 200 个测试，适合自学。

前面几次的作业偏 PL 理论，后面几次的作业偏系统编程。如果你觉得前面几次的课程内容和作业过于理论，可以重点尝试使用 OCaml 实现解释器的作业，它既能让你对之前的理论有更深刻的理解，又能让你实战一个函数式语言的类型检查和解释。

而后面的作业则更倾向于利用理论来指导系统编程与设计，尤其是 Rust 和它独特的所有权机制与类型系统。虽然我们要经常与编译器搏斗，但这也恰好说明了类型系统和理论对于编程和设计的意义。

个人自学过程中感觉作业还是偏难的，但收获很大，在后续作业的编程实践和前面所学的理论知识产生交集时会有恍然大悟的愉悦。如果你在完成作业时遇到了困难，这是十分正常的，请静下心来认真思考，或者再读一遍实验指导。

课程资源

课程网站：官网
课程视频：无，主要学习途径是课程笔记和完成作业
课程教材：前半部分是著名的TAPL，后半部分则无固定教材
课程作业：实验指导与作业仓库

NJU: 软件分析

课程简介

所属大学：南京大学
先修要求：数据结构与算法，至少熟悉一门编程语言
编程语言：Java
课程难度：🌟🌟🌟
预计学时：60 小时

软件分析是由南京大学李樾老师和谭添老师共同开设的一门课程，主要介绍了程序分析，在这里特指静态分析的理论与实践。静态分析的理念是在不运行程序的情况下，通过分析其源代码和各种表示来获得关于程序特定性质的近似结论。这门课从程序的抽象语法树，控制流图和中间表示这些基础知识开始介绍，再到数据流分析和指针分析的理论与实践，最后介绍了若干高级主题，如 IFDS 等。

这门课程值得学习的原因在我看来有两部分：

授课。程序分析一般来说并不太好上手，但两位老师讲的尤其细致入微，还会在课上带你一步一步走某一个算法的流程。个人认为只要认真听课，对于课上的知识不存在学不懂或者讲的不清楚的问题。
作业。作业围绕其自创的 Java 程序分析框架太阿进行。八个作业涵盖多种静态分析技术，包括编译优化（活跃变量分析、常量传播、死代码检测），基础程序分析（程序调用图构建、非/上下文敏感指针分析），以及程序分析在软件安全性的应用（污点分析）。课程同时还提供所有人可用的在线评测系统，适合自学。

作业主要是实现课上的伪代码算法，从而更好的帮助你理解课上所讲的知识。我感觉难度并不是特别大，特别适合在上完课后完成对应的实验来检验自己对课上知识的掌握程度。不过想要通过每个作业的所有测试点还是很有难度的。

课程资源

课程网站：主页
课程视频：Bilibili
课程教材：无
课程作业：实验主页
在线评测： OJ

PKU: 软件分析技术

课程简介

所属大学：北京大学
先修要求：数据结构与算法，至少熟悉一门编程语言
编程语言：Java, Python
课程难度：🌟🌟🌟🌟
预计学时：60 小时

软件分析技术是由北京大学熊英飞老师开设的一门课程，主要介绍了以下内容：

基于抽象解释的程序分析（数据流分析、过程间分析、指针分析、抽象解释等）
基于约束求解的程序分析（SAT、SMT、符号执行等）
软件分析应用（程序合成、缺陷定位、缺陷修复等）

和南京大学的软件分析课程对比，这门课程的特点是讲了更多更全面的程序分析的理论与实践相关内容，难度也更大。这门课程我的主要的学习途径是听课，熊老师上课十分有趣，除了理论内容讲的很好偶尔也会讲一些学术相关的小段子:)

而本实验的的课程项目是实现一个Java上的指针分析系统和一个程序合成工具，也是十分有趣的实践。

课程资源

课程网站：主页这是 2020 年的课程主页，在熊老师的主页上可以找到更多年份的课程内容。
课程视频：2020 燕云直播
课程教材：无

Cambridge: Semantics of Programming Languages

课程简介

所属大学：University of Cambridge
先修要求：基础离散数学
编程语言：OCaml/ML
课程难度：🌟🌟🌟
预计学时：20 至 30 小时

这门课程系统性地讲述了编程语言中的语义学 (Semantics)。它在定义和设计语言的背景下，为编程语言的构造和规范声明提供了一个非常适合初学者，但同样严谨且形式化的介绍。这也是为数不多的提供公开视频的编程语言理论课程之一。

课程内容涵盖了从操作语义 (Operational Semantics) 到指称语义 (Denotational Semantics) 的各个主题。课程开始会先介绍一个使用 BNF 约束的简单命令式语言的基本操作语义，然后逐步引入形式类型系统，使用归纳法，特别是结构归纳法 (Structural Induction) 来构建基于规则的归纳证明，介绍了程序语言语义学中的许多基本性质及其证明。然后讨论在函数式编程视角下如何操作数据，并介绍着重子类型和函数处理。最后讨论语义等价性、一致性性质以及在并发环境下的语义学。

这门课在校内面向二年级本科生，难度不高，但同时引入了一些非常重要的概念。它将是进一步研究类型理论、范畴理论、霍尔逻辑和模型检测的关键要素。