| 日期 | 内容 |
|---|---|
| 7月19日 | 课程介绍 |
| Overview | |
| 函数式程序设计 | |
| 实验一(demo.ml) | |
| 7月20日 | Curry-Howard Isomorphism |
| 证明辅助工具Coq介绍 | |
| 实验二 实验二答案 | |
| 7月21日 | 出具证明编译器 |
| 实验三 实验三答案 | |
| 7月22日 | 自动定理证明器 |
| 实验四(第一部分) | |
| 7月23日 | 并发程序验证 |
| 实验四(第二部分) | |
| 7月24日 | Modular Development of Certified System Software |
| 并发程序验证 | |
| 实验五(PPT) | |
| 7月25日 | Modular Development of Certified System Software |
| Attachment | Size |
|---|---|
| Lecture1.ppt | 667 KB |
| ProofGeneral.rar | 2.29 MB |
| dotemacs.rar | 206 bytes |
| tuareg.rar | 26.24 KB |
| Lab1.rar | 23.58 KB |
| Intro.ppt | 482 KB |
| Lec1-Overview.pdf | 485.47 KB |
| Lec2-CurryHoward.pdf | 374.34 KB |
| coq.ppt | 842 KB |
| logic_prac.rar | 4.44 KB |
| logic_solution.rar | 4.69 KB |
| certifyingcompiler.ppt | 856.5 KB |
| lab3_final.zip | 25.47 KB |
| lab3_solution.zip | 1.84 KB |
| Lecture4.zip | 3.88 MB |
| lab4.zip | 31.8 KB |
| concurrency.pdf | 1.42 MB |
| lab5.zip | 5.75 KB |
| ESC.ppt | 305.5 KB |
| Lec5-6.pdf | 3.22 MB |