程序设计语言的形式语义

本课程属于本研贯通课程，具有一定的难度。

本课程为理论性课程，要求学习者具备一定的数学基础，尤其需要熟悉命题逻辑相关的内容（推荐先修：数理逻辑）。

梁老师为大一学生开设的青春版课程“青年科光——程序设计语言珠玑”，主题与本课程基本一致，而本课程在此基础上进行了更多拓展与拔高。如果同学们在大一时已经选修过“青年科光”，那么学习这门课程可能会感觉更为轻松。

梁老师人很好，有板书，讲课有录屏回放。

25 秋季情况¶

每周三早八上课，起不来可以看录屏回放，但相应地就看不到板书，且设备有（比较大）可能翻车，还是强烈推荐现场听课的。

讲课内容为：

Lambda calculus - Untyped lambda calculus - Simply-typed lambda calculus - System F - System Omega

Imperative languages - Operational semantics (small step semantics and big step semantics) - Hoare logic

C-like pointer programs and separation logic

25 秋季共有 4 次作业，时限都是一周，无特殊理由不可补交。助教批改作业很认真很严格，只接受 formal 的答案。建议务必充分弄懂作业内容。

平时分完全由作业决定，无期中考。总评分数计算：

if 平时成绩 < 期末考试成绩 then:
  总评成绩 = 期末考试成绩
else:
  总评成绩 = 平时成绩 * 40% + 期末考试成绩 * 60%

期末考试为闭卷考试，全英文试卷。试卷首先举了一个和课上所讲的类似但更为综合和拔高的编程语言，给出其语义以及 Type Derivation，然后基于此询问有关该语言的若干问题。

以下摘自最后一堂课的 course review 的 PPT：

If I show you a formal system, can you apply it to examples? - Given a small-step operational semantics, write down a full execution path of a program from an initial state - Given a big-step operational semantics, write down the derivation of a big-step transition - Given a type system, write down the typing derivation - Given a program logic, write down the proof of a specification - Given a definition of a property, tell whether it holds

If I tell you the informal meaning of a property, can you formalize it? - Please do not use natural language in your formalization

可参考 box 往年卷，出题形式基本类似。体感上今年比往年难。

（应该）不捞人（ps：据小道消息，实际上是捞了的，改了给分比例把作业比例占分增加了不少）。据老师说，对于研究生同学，如果总评不及格，老师会默认在系统中标注“未上课”不录入成绩；对于本科生同学暂不清楚是否有类似做法。考完可以跟老师问成绩，老师还会告诉你哪里写错了。

接下来是经典选不选环节。

首先声明写这一段的作者不是写上面内容的作者。这门课： - 帮你用非常formal、数学的全新视角重新看待编程语言，避免一切感性 - 能够学到实用的理论（例如inference rule），学完后你甚至可以把学到的理论推广到自然语言、生活中去 - 学到的内容可以帮助你看懂PL和程序验证相关的论文 - 可以为你写编译器/解释器提供理论指导和思路 - 是国内乃至世界内都少有教授的主题 但是： - 比较hardcore/数学，有一定理解难度 - 早八

程序设计语言的形式语义

25 秋季情况¶

评论