Chapter 1
Introduction
先交代课程脉络、资料来源与阅读顺序，方便后面逐章推进。
专栏章节导航
章节按列表排列，点击任意标题即可跳转到对应文章或章节页。
Chapter 2
ch1-2 数理逻辑
先把命题逻辑和谓词逻辑记号收拢好，为后续证明与推导热身。
Chapter 3
ch3 集合论
用集合论把后续语义里的记号系统打底，减少推导时的卡顿感。
Chapter 4
ch4 操作语义
从抽象机视角进入操作语义，看大步与小步规则如何展开程序执行。
Chapter 5
ch5 归纳原理
把归纳法的常见证明套路整理成工具箱，方便后续直接调用。
Chapter 6
ch6 归纳定义
围绕规则归纳、算子与不动点，为后面的指称语义提前铺路。
Chapter 7
ch7 指称语义
聚焦指称语义里最核心的定义、公式和考试高频考法。
Chapter 8
ch8 公理语义
把霍尔逻辑规则和典型做题入口整理成一份可直接套用的笔记。
Chapter 9
ch9 lambda演算
从最基础的 λ 表达式出发，理解归约规则和计算直觉。
Chapter 10
Lambda 演算归约练习
用 8 道练习题集中训练 α/β 变换与变量捕获规避的手感。
Chapter 11
Rocq知识点
把 Rocq/Coq 常用命令、策略和易错点压成一份速查清单。
Chapter 12
Rcoq模拟题
两套 Rocq 模拟题，适合在做题中熟悉命令、策略和逻辑基础。
Chapter 13
大步语义推导树练习
用 Aexp、Bexp 和循环语句例子练习大步语义推导树的写法。
Chapter 14
小步语义格局变换练习
通过格局变换题练熟小步语义，尤其是“每一步怎么写”。
Chapter 15
等价性证明练习
结合顺序、条件和 while 例子，练习程序等价性的证明思路。