CS 2205, PLDI, Fall 2025

Instructor: Qinxiang Cao (曹钦翔)

TAs: Xiwei Wu(吴熙炜) Kan Liu(刘衎)
Lectures
Time 1: Tuesday 10:00-11:40
Time 2: Thursday 10:00-11:40 (odd weeks)
Location: East Down Hall (东下院) 209
Email: caoqinxiang@sjtu.edu.cn


Extended Reading

  1. Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction.
  2. Appel, Andrew W. Modern Compiler Implementation in C.

Course Supplements

  1. Coq-8.20安装文件（下载）
  2. SetsClass库（下载）

Course Projects

  1. General Info （下载）
  2. Problem List of Programming Tasks: （下载）
  3. Problem List of Theory Tasks: （下载）

Lecture Schedule

Week Date Lecture Notes Attachments Homework
1 09/16    课程信息简介. pdf

 

 
   词法分析. pdf

 

link
09/18

词法分析器示例. zip

link
   语法分析. pdf

 

link
2 09/23

 

link
3 09/28

语法分析器示例. zip

link
09/30    程序语言语法的Coq定义. pdf / v

简单Coq证明与定义. pdf / v
课后阅读：高阶函数与高阶谓词. pdf / v
课后阅读：Coq中的归纳类型. pdf / v

link
link
5 10/14    表达式指称语义. pdf / v

课后阅读：Coq中的rewrite证明指令. pdf / v
课后阅读：Coq中的代数结构. pdf / v

link
link
10/16

 

link
   利用集合与关系定义指称语义. pdf / v

Coq中的集合与关系. pdf / v

 
6 10/21

 

link
link
7 10/28

Coq标准库中的自然数. pdf / v
课后阅读：集合与关系运算性质的证明方法. pdf

link
10/30

Coq中的结构归纳法证明. pdf / v
Coq中的逻辑证明. pdf / v

link
8 11/04    霍尔逻辑. pdf

课后阅读：符号执行. pdf

link
9 11/11    用单子表示计算. pdf / v

 

link
11/13

课后阅读：WhileD表达式指称语义. pdf / v

 
10 11/18    不动点定理. pdf / v

课后阅读：在Coq中证明Kleene不动点定理. pdf / v

link
11 11/25

 

link
11/27    单子程序上的霍尔逻辑. pdf / v

 

 
12 12/02

 

link
13 12/09

 

link
12/11

 

 
14 12/16    状态关系单子与霍尔逻辑. pdf / v