程序设计语言理论（冯新宇）
2017春 2015春 课程号：CS0511501
2017春 2015春 课程号：CS0511501
2017春 2015春 课程号：CS0511501
10.0(1人评价)
10.0(1人评价)
- 课程难度：困难
- 作业多少：很多
- 给分好坏：一般
- 收获大小：很多
| 选课类别：基础 | 教学类型：理论课 |
| 课程类别：研究生课程 | 开课单位：计算机科学与技术系 |
| 课程层次：硕士 | 学分：3.0 |
点评
写点评
排序
学期
评分
评分
1条点评
- 课程难度：困难
- 作业多少：很多
- 给分好坏：一般
- 收获大小：很多
- 难度：困难
- 作业：很多
- 给分：一般
- 收获：很多
这门课是讲 Coq 形式化证明。内容涵盖了程序设计语言理论的多个方面，上完这门课大概就入门了这个研究领域。作业是用 Coq 写证明，由于跟命令式编程语言的思维方式不同，需要比较长的时间才能写出来。
冯教授上课经常用投影现场写代码或者展示代码，因此要坐在比较靠前的位置才能看清。不过这不是个问题，因为这门课选课的人数通常很少，第一节课就会吓跑一半多人。课程有难度，选课需谨慎！
课程主页： http://staff.ustc.edu.cn/~xyfeng/teaching/TOPL/
教材：经典 Benjamin C. Pierce, et al. Software Foundations (local copy: gz file or rar file).
PPT：
- 01_Introduction.pdf
- 02_CoqOverview.pptx
- 03_Math.pdf
- 04_lambda.pdf （lambdanotes.pdf）
- 05_type.pdf
- 05_typesafe.pdf
- 05_typesafe_proof.pdf
- 06_operational.pdf
- 07_Hoare.pdf
- 08_separation.pdf
- 09_Concur_Semantics.pdf
- 10_Concurrency_Lin.pdf
- ConcurVerification.ppt
