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