CS 2206, Programming Verification, Spring 2025

Instructor: Qinxiang Cao (曹钦翔)

TAs: Chengxi Yang (杨承羲)
Lectures
Time: Tuesday 18:00-19:40, Friday 8:00-9:40 (odd weeks)
Location: East Down Hall (东下院) 407
QQ Group: 200073830
Email: caoqinxiang@sjtu.edu.cn


Extended Reading

  1. Pierce, Benjamin, et. al. Software Foundation.
  2. Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction.
  3. Harper, Robert. Practical Foundations for Programming Languages.

Course Supplements

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

Final project

  1. To be released

Lecture Schedule

Week Date Lecture Notes Homework Attachments
1 02/18    课程信息简介. pdf / v      
   课后阅读：简单Coq证明与定义. pdf / v      
   Coq归纳类型. pdf / v      
02/21    link   
   程序语言的语法. pdf / v      
   课后阅读：用递归函数定义数学性质. pdf / v      
2 02/25    整数类型表达式的指称语义. pdf / v    link   
   课后阅读：布尔类型表达式的指称语义. pdf / v    link   
   课后阅读：Coq标准库中的自然数. pdf / v      
3 03/04    课后阅读：逻辑命题的证明. pdf / v      
   基于关系的指称语义. pdf / v    link   
03/07    link   
4 03/11    不动点定理. pdf / v    link   
5 03/18    霍尔逻辑. pdf / v    link   
03/21      
6 03/25    link   
7 04/01    用单子描述计算. pdf / v      
8 04/08    link   
   课后阅读：Coq标准库中的列表. pdf / v      
9 04/15    分离逻辑. pdf      
04/18