JF叫我暑假看看这个 也该填这个坑了
（进了dev repo 有答案咯！）
相关课程
Upenn CIS500 Pierce直接教的 现在网站好像挂了 可以去web archive找
P大的课 相似的进度/材料 有中文slides
希望暑假能跟着课读书做题。
Notes
比较值得讲的题： Binary Inverse, Church Numerals P大的习题课讲过
LF
书的结构
Part 1: intro to coq
Basics, Induction, Lists, Poly, Tactics
Part 2: Propositions (and more induction)
Logic, IndProp, ProofObjects, IndPrinciples
其中IndProp是大chapter （其实Logic最后一题也被我跳了）
Part 3: Imp
Maps, Imp, ImpCEvalFun, Auto
其中Imp是大chapter
PLF
书的结构
Part 1: Verification (Hoare Logic)
Equiv, Hoare, Hoare2, HoareAsLogic
Part 2: Type System (STLC)
Smallstep, Types, Stlc, StlcProp