PL 19
- Denotational Semantics of Typed Lambda Calculus V — CPO Model for Imperative Programs
- Denotational Semantics of Typed Lambda Calculus IV — CPO Model for PCF
- Denotational Semantics of Typed Lambda Calculus III — Full Continuous Hierarchy
- Denotational Semantics of Typed Lambda Calculus II — Partial Orders and Continuous Functions
- Denotational Semantics of Typed Lambda Calculus I — Henkin Models
- 类型化 Lambda 演算的指称语义：五篇文章的进阶路线
- Easy Foundations for Programming Languages X — Imperative Programs
- Easy Foundations for Programming Languages IX — Universal Algebra and Algebraic Data Types
- Easy Foundations for Programming Languages VIII — Proof Systems
- PLDI 2023 Distinguished Papers Comments
- Easy Foundations for Programming Languages VII — Simply-Typed Lambda Calculus
- Easy Foundations for Programming Languages VI — PCF Extensions (Unit, Sum, Recursive Types)
- Easy Foundations for Programming Languages V — PCF Iteration and Recursion
- Easy Foundations for Programming Languages IV — PCF Semantics
- Easy Foundations for Programming Languages III — The Language PCF & Its Syntax
- Easy Foundations for Programming Languages II — Notation and Mathematical Conventions
- Easy Foundations for Programming Languages I — Introduction
- Programming Language Pragmatics
- 程序语言基础：从语法、语义到命令式程序的阅读地图