Summer School 2010
Sun, 09/19/2010 - 20:15 — apostate
暑期实践课程
1 课程安排
| 日期 | 内容 |
|---|---|
| 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 |
2 Emacs
- 下载Emacs,解压到任意路径.
- 下载".emacs"
- 设置环境变量HOME为".emacs"文件所在目录.
- 下载"tuareg-mode"和"proofgeneral",并解压缩到Emacs/site-lisp
- 根据解压的路径修改".emacs"
4 OCaml资料
- A Tutorial Website for OCaml
5 Coq资料
- Quick reference of tactics
- Manual
- Coq In a Hurry
6 ESC/Java安装
- Login to post comments