CS 2612, Programming Languages and Compilers, Fall 2025

Instructor: Qinxiang Cao (曹钦翔)

TAs: Zhang Cheng(程章) Zhehao Li(李喆浩)
Lectures
Time 1: Wednesday 10:00-11:40
Time 2: Friday 8:00-9:40
Location: East Middle Hall (东中院) 3-206
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. To Be Released

Course projects

  1. To Be Released

Lecture Schedule

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

 

 
   词法分析. pdf

 

link
09/19

词法分析器示例. zip

link
   语法分析. pdf

 

link
2 09/24

 

link
09/26

语法分析器示例. zip

link
4 10/10    简单编译器. pdf

 

link
10/11    程序语言语法的Coq定义. pdf / v

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

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

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

link
link
10/17

 

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

在Coq中表示集合. pdf / v

 
6 10/22

Coq中的集合证明方法汇总. pdf

link
link
10/24

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

link
7 10/29

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