Cambridge: Semantics of Programming Languages
课程简介
- 所属大学：University of Cambridge
- 先修要求：基础离散数学
- 编程语言：OCaml/ML
- 课程难度：🌟🌟🌟
- 预计学时：20 至 30 小时
这门课程系统性地讲述了编程语言中的语义学 (Semantics)。它在定义和设计语言的背景下，为编程语言的构造和规范声明提供了一个非常适合初学者，但同样严谨且形式化的介绍。这也是为数不多的提供公开视频的编程语言理论课程之一。
课程内容涵盖了从操作语义 (Operational Semantics) 到指称语义 (Denotational Semantics) 的各个主题。课程开始会先介绍一个使用 BNF 约束的简单命令式语言的基本操作语义，然后逐步引入形式类型系统，使用归纳法，特别是结构归纳法 (Structural Induction) 来构建基于规则的归纳证明，介绍了程序语言语义学中的许多基本性质及其证明。然后讨论在函数式编程视角下如何操作数据，并介绍着重子类型和函数处理。最后讨论语义等价性、一致性性质以及在并发环境下的语义学。
这门课在校内面向二年级本科生，难度不高，但同时引入了一些非常重要的概念。它将是进一步研究类型理论、范畴理论、霍尔逻辑和模型检测的关键要素。