|
Extended Reading
- Pierce, Benjamin, et. al. Software Foundation.
- Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction.
- Harper, Robert. Practical Foundations for Programming Languages.
Course Supplements
Final project
- To be released
Lecture Schedule
| Week |
Date |
Lecture Notes |
Attachments |
Homework |
| 1 |
03/04 |
程序语言语法的Coq定义. pdf / v |
简单Coq证明与定义. pdf / v
课后阅读：高阶函数与高阶谓词. pdf / v
课后阅读：Coq中的归纳类型. pdf / v |
|
| 03/06 |
表达式指称语义. pdf / v |
课后阅读：Coq中的rewrite证明指令. pdf / v
课后阅读：Coq中的代数结构. pdf / v |
link
link |
| 2 |
03/13 |
|
link |
| 利用集合与关系定义指称语义. pdf / v |
Coq中的集合与关系. pdf / v |
link |
| 3 |
03/18 |
课后阅读：Coq标准库中的自然数. pdf / v |
link |
| 03/20 |
课后阅读：集合与关系运算性质的证明方法. pdf
课后阅读：Coq中的结构归纳法证明. pdf / v
课后阅读：Coq中的逻辑证明. pdf / v |
|
| 4 |
03/27 |
霍尔逻辑. pdf |
|
link |
| 5 |
04/01 |
课后阅读：反向赋值语句推理规则. pdf |
link |
| 04/03 |
用单子表示计算. pdf / v |
|
|
| 6 |
04/10 |
课后阅读：WhileD表达式指称语义. pdf / v |
link |
|