这是 thesis Self Adjusting Computation 的阅读笔记。“重新发明” 指的是尝试从要解决的问题出发，用推导的方式一步步构建出论文中的解决方案。
pdf这是对经典论文 On the Expressive Power of Programming Languages 及其衍生思想的一份个人诠释， 介绍了比较语言功能的表达能力、严谨地定义“语法糖”这一概念的方式，以及由此衍生的设计新编程语言的方法论。
html介绍了 logical relation 的方法在 PL 中的各种应用。 Logical relation 在研究语言的语义和类型系统的性质是非常常见且使用的方法。 本文介绍它的各种变种和许多不同的常见应用
pdf对 Normalization-By-Evaluation（NBE）这一类 normalization 算法进行简单介绍。 主要侧重于 NBE 的定义、原理和不同变种，不涉及正确性证明的内容。
pdf对类型论中等式类型的各种变种进行走马观花式的简单介绍。 包括 intensional/extensional equality 及其各种变种、 observational equality 以及 HoTT/Cubical TT 等。
pdf尝试沿着编程语言和 universal algebra 的联系的思路， 把多种编程语言构造和数学构造串连在一起。 包括 Abstract/Algebraic Data Type、recursion scheme、algebraic effect、CBPV、 universal algebra、F-algebra、monad、adjunction 等
pdf介绍“family”和“fibration”这两个概念的联系， 以及这一联系在集合论、范畴论、类型论中的体现， 并基于这一点介绍了类型论的常见范畴语义， 以及 dependent type 中的基本构造在范畴语言中的翻译。
pdf对 Stephen Dolan 的 thesis “Algebraic Subtyping”的介绍。 这篇论文做出了 parametric polymorphism + subtyping 的 sound、complete、principal 的类型推导。 而且它使用的的思想与方法十分有趣。
pdf试图一步步地，沿着“用范畴论的语言描述 STLC”的思路， 推导出 Cartesian Closed Category 的构造。
html