跳转至

Cambridge: Semantics of Programming Languages

约 460 个字 预计阅读时间 2 分钟

课程简介

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

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

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

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

课程资源

  • 课程网站:Latest
  • 课程视频:YouTube
  • 课程教材:
  • Pierce, B.C. (2002). Types and programming languages. MIT Press.
  • Winskel, G. (1993). The formal semantics of programming languages. MIT Press.
  • 课程作业:考试真题中的相关题目汇总在 这里,但是相关作业题 (Cambridge 内部的 supervision) 以及所有题目的答案均不公开。