结合顺序、条件和 while 例子，练习程序等价性的证明思路。
2026-02-03
小步语义格局变换练习
通过格局变换题练熟小步语义，尤其是“每一步怎么写”。
2026-02-02
大步语义推导树练习
用 Aexp、Bexp 和循环语句例子练习大步语义推导树的写法。
2026-02-01
Rocq知识点
把 Rocq/Coq 常用命令、策略和易错点压成一份速查清单。
2026-01-31
Rcoq模拟题
两套 Rocq 模拟题，适合在做题中熟悉命令、策略和逻辑基础。
2026-01-30
Lambda 演算归约练习
用 8 道练习题集中训练 α/β 变换与变量捕获规避的手感。
2026-01-29
ch9 lambda演算
从最基础的 λ 表达式出发，理解归约规则和计算直觉。
2026-01-28
ch8 公理语义
把霍尔逻辑规则和典型做题入口整理成一份可直接套用的笔记。
2026-01-27
ch7 指称语义
聚焦指称语义里最核心的定义、公式和考试高频考法。
2026-01-26
ch6 归纳定义
围绕规则归纳、算子与不动点，为后面的指称语义提前铺路。
2026-01-25
ch5 归纳原理
把归纳法的常见证明套路整理成工具箱，方便后续直接调用。
2026-01-24
ch4 操作语义
从抽象机视角进入操作语义，看大步与小步规则如何展开程序执行。
2026-01-23