CS 2612, Programming Languages and Compilers, Fall 2024

Instructor: Qinxiang Cao (曹钦翔)

TAs: Xiwei Wu(吴熙炜) Jiyang Wu(吴基洋)
Lectures
Time 1: Wednesday 10:00-11:40
Time 2: Friday 8:00-9:40
Location: East Middle Hall (东中院) 4-504
QQ Group: 1007523862
Email: caoqinxiang@sjtu.edu.cn


Extended Reading

  1. Harper, Robert. Practical Foundations for Programming Languages.
  2. Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction.
  3. Pierce, Benjamin, et. al. Software Foundation.
  4. Appel, Andrew W. Modern Compiler Implementation in C.

Course Supplements

  1. SetsClass库（下载）
  2. CompCert项目中的64位整数库（下载）

Course projects

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

Lecture Schedule

Week Date Lecture Notes Homework Attachments
1 09/20    课程信息简介. pdf      
   词法分析. pdf    link   
2 09/25    link    link
09/27    语法分析. pdf      
4 10/09    link   
10/11    link    link
5 10/16    简单编译器. pdf    link   
10/18    link   
   简单Coq证明与定义. pdf / v    link   
6 10/23      
   Coq中的归纳类型. pdf / v      
   课后阅读：用递归函数定义数学性质. pdf / v    link   
   程序语言语法的Coq定义. pdf / v      
10/25    指称语义. pdf / v      
7 10/30    link   
   课后阅读：Coq标准库中的自然数. pdf / v    link   
   基于关系的指称语义. pdf / v      
11/01      
8 11/06    link   
   课后阅读：逻辑命题的证明. pdf / v      
11/08    大作业信息. pdf      
   不动点定理. pdf / v      
9 11/13    link   
11/15    霍尔逻辑. pdf    link   
10 11/20    link   
11/22    用单子描述计算. pdf / v      
11 11/27    link   
   课后阅读：Coq列表. pdf / v    link   
11/29    用单子描述计算2. pdf / v      
12 12/04      
   分离逻辑. pdf      
12/06      
13 12/11      
12/13    表示谓词. pdf      
14 12/18      
12/20      
15 12/25      
12/27    含程序状态的单子. pdf / v      
16 01/03