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      
   指称语义. pdf / v