diff --git a/docs/编程语言设计与分析/Cambridge-Semantics.en.md b/docs/编程语言设计与分析/Cambridge-Semantics.en.md new file mode 100644 index 00000000..763d1f10 --- /dev/null +++ b/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. diff --git a/docs/编程语言设计与分析/Cambridge-Semantics.md b/docs/编程语言设计与分析/Cambridge-Semantics.md new file mode 100644 index 00000000..824de6cb --- /dev/null +++ b/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) 以及所有题目的答案均不公开。 diff --git a/mkdocs.yml b/mkdocs.yml index c18d0638..970d063b 100644 --- a/mkdocs.yml +++ b/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"