Software Foundations

 

JF叫我暑假看看这个 也该填这个坑了

书的网址

(进了dev repo 有答案咯!)

相关课程

Upenn CIS500 Pierce直接教的 现在网站好像挂了 可以去web archive找

P大的课 相似的进度/材料 有中文slides

希望暑假能跟着课读书做题。

知乎上的coq贴

CSE505 UW Sp 2021

CSE505 UW 18au

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