[COURSE] Add Cambridge: Semantics of Programming Languages (PKUFlyingPig#615)

* feat: added "semantics of programming languages" course

* fix: fixed format errors as suggested

Author: YunkaiZhang233

docs/编程语言设计与分析/Cambridge-Semantics.en.md

@@ -0,0 +1,24 @@
+# Cambridge: Semantics of Programming Languages
+
+## Descriptions
+
+- Offered by: University of Cambridge
+- Prerequisites: elementary Discrete Mathematics, including logic and proof methodology, basic functional programming
+- Programming Languages: OCaml (ML)
+- Difficulty: 🌟🌟🌟
+- Class Hour: 20 to 30 hours (12 hours of lecture)
+
+This course offers a structural, operational approach to programming language semantics. It provides a very beginner-friendly but mathematically rigorous introduction to the constructs and specification declaration of programming languages, in the context of actually defining and designing a language. It is also one of the few PLT courses that offers publicly available videos.
+
+The course covers semantics topics ranging from operational and denotational semantics. The course starts with introducing the basic operational semantics of a simple imperative language defined by BNF, and gradually coming to introducing formal type systems, using mathematical induction (especially structural induction) to build rule-based induction proofs. It then comes to how we manipulate data under a functional programming perspective and introduces subtyping and handling of functions. Finally it comes to the discussion of semantics equivalence, congruence property and semantics under concurrency.
+
+This course was taught to 2nd year undergraduate students, however building up some very important concepts. It would be a pivotal capstone for further studies on type theory, category theory, hoare logic and model checking.
+
+## Course Resources
+
+- Course Website: [Latest](https://www.cl.cam.ac.uk/teaching/2324/Semantics/)
+- Recordings: [YouTube](https://www.youtube.com/playlist?list=PL-2hPK7m5S3hVagseKDPxCBZEqg0PqZhs)
+- Textbooks:
+  - Pierce, B.C. (2002). _Types and programming languages_. MIT Press.
+  - Winskel, G. (1993). _The formal semantics of programming languages_. MIT Press.
+- Assignments: Related Past Paper Questions are listed [here](https://www.cl.cam.ac.uk/teaching/exams/pastpapers/t-SemanticsofProgrammingLanguages.html), however solutions and tutorial sheets are visible to internal students only.

docs/编程语言设计与分析/Cambridge-Semantics.md

@@ -0,0 +1,24 @@
+# Cambridge: Semantics of Programming Languages
+
+## 课程简介
+
+- 所属大学：University of Cambridge
+- 先修要求：基础离散数学
+- 编程语言：OCaml/ML
+- 课程难度：🌟🌟🌟
+- 预计学时：20 至 30 小时
+
+这门课程系统性地讲述了编程语言中的语义学 (Semantics)。它在定义和设计语言的背景下，为编程语言的构造和规范声明提供了一个非常适合初学者，但同样严谨且形式化的介绍。这也是为数不多的提供公开视频的编程语言理论课程之一。
+
+课程内容涵盖了从操作语义 (Operational Semantics) 到指称语义 (Denotational Semantics) 的各个主题。课程开始会先介绍一个使用 BNF 约束的简单命令式语言的基本操作语义，然后逐步引入形式类型系统，使用归纳法，特别是结构归纳法 (Structural Induction) 来构建基于规则的归纳证明，介绍了程序语言语义学中的许多基本性质及其证明。然后讨论在函数式编程视角下如何操作数据，并介绍着重子类型和函数处理。最后讨论语义等价性、一致性性质以及在并发环境下的语义学。
+
+这门课在校内面向二年级本科生，难度不高，但同时引入了一些非常重要的概念。它将是进一步研究类型理论、范畴理论、霍尔逻辑和模型检测的关键要素。
+
+## 课程资源
+
+- 课程网站：[Latest](https://www.cl.cam.ac.uk/teaching/2324/Semantics/)
+- 课程视频：[YouTube](https://www.youtube.com/playlist?list=PL-2hPK7m5S3hVagseKDPxCBZEqg0PqZhs)
+- 课程教材：
+  - Pierce, B.C. (2002). _Types and programming languages_. MIT Press.
+  - Winskel, G. (1993). _The formal semantics of programming languages_. MIT Press.
+- 课程作业：考试真题中的相关题目汇总在 [这里](https://www.cl.cam.ac.uk/teaching/exams/pastpapers/t-SemanticsofProgrammingLanguages.html)，但是相关作业题 (Cambridge 内部的 supervision) 以及所有题目的答案均不公开。

mkdocs.yml

@@ -238,6 +238,7 @@ nav:
       - "Stanford CS242: Programming Languages": "编程语言设计与分析/CS242.md"
       - "NJU 软件分析": "编程语言设计与分析/NJU-SoftwareAnalysis.md"
       - "PKU 软件分析": "编程语言设计与分析/PKU-SoftwareAnalysis.md"
+      - "Cambridge: Semantics of Programming Languages": "编程语言设计与分析/Cambridge-Semantics.md"
   - 计算机图形学:
       - "GAMES101": "计算机图形学/GAMES101.md"
       - "GAMES202": "计算机图形学/GAMES202.md"