- Homotopy Type Theory Univalent Foundations of Mathematics
- An Introduction to Homological Algebra
- Computational Category Theory
- 编程视角下的范畴和函子
- 编程视角下的余极限和极限
- 逻辑和Topos
- Introduction to Higher-Order Categorical Logic
- A Course in Mathematical Logic for Mathematicians
- 什么是语言？
- 计算理论视角下的群
- An Introduction to Proof Theory
- 什么是证明？
- 自然演绎
- Interactive Models of Computation and Program Behavior
- Temporal Logic and State Systems
- Formal Methods for Software Engineering
- 进程代数——CSP
- 代数规范——CASL
- Foundations of Algebraic Specification and Formal Software Development