- Program = Proof
- 程序即证明
- 证明助手
- 同伦类型和形式化证明
- Lambda演算
- 无类型的Lambda演算
- 简单类型的Lambda演算
- 从低阶类型到高阶类型
- Coq证明助手和形式化证明
- Algorithmic Information Theory
- Quantum Computation and Quantum Information
- Introduction to the Theory of Computation
- 有限自动机和正则表达式
- 下推有限自动机和上下文无关语法
- Turing机和算法
- Introduction to the Theory of Programming Languages
- 从不动点定理到编程语言
- 可计算函数的编程语言PCF
- PCF的解释
- Writing An Interpreter In Go
- 编程语言Monkey的词法分析
- Programming Languages Application and Interpretation
- 从求值器到编译器