书
Category Theory for Programmers: The Preface | Bartosz Milewski's Programming Cafe
[A taste of category theory for computer scientists](A taste of category theory for computer scientists)
最近在整理资料时候发现一本早就加入 waiting list 的书：《Programming Languages: Build, Prove, and Compare》（下称 PLBPC）已经出版了，读了一下觉得很适合拿它来回答这个问题。
PFPL, TAPL
- TAPL 以类型系统为脉络贯穿全书，介绍了类型系统的方方面面，并随附了对应类型系统实现的代码，适合泛 PL 或类型系统方面研究入门
- PFPL 以一种很像“字典”的形式简洁地涵盖所有编程语言相关特性的语义的形式化理论内容，包含定理与证明，也对得起标题中的 Foundation。但如果没有好的带路人很难靠这个独立学习。
An Introduction to Proof Theory: Normalization, Cut-elimination, and Consistency Proofs