一个临时的目录
Ⅰ. 逻辑与数学基础
- 命题与谓词逻辑
- 自然演绎系统：引入/消除规则，构造可靠证明树
- 语义模型：塔斯基真值定义，一阶结构的解释
- 类型论基础
- λ立方体（Lambda Cube）：从简单类型到依赖类型的层次化扩展
- 同伦类型论（HoTT）：类型作为空间，命题类型的路径解释
- 代数规约方法
- 初始语义（如 OBJ 语言的方程规约）
- 行为抽象：用不变式（Invariants）定义系统边界
- 基于逻辑的规约语言
- 时序逻辑（LTL/CTL）：刻画程序动态行为（
◇□P类时态公式）
- 分离逻辑（Separation Logic）：描述堆内存结构的推理规则
Ⅲ. 程序验证技术
- 静态验证方法
- 演绎验证（Deductive Verification）：通过霍尔逻辑（Hoare Logic）生成验证条件（VC）
- 抽象解释（Abstract Interpretation）：利用格理论（Lattice）近似程序行为
- 动态验证方法
- 符号执行（Symbolic Execution）：路径条件的约束求解（与 SMT 理论结合）
- 模型检验（Model Checking）：通过状态空间遍历验证时态逻辑属性
Ⅳ. 类型系统方法论
- 类型安全性证明技术
- 进步与保持定理（Progress & Preservation）：通过结构归纳法证明类型系统健全性
- 类型擦除与擦除语义：证明类型无关运行结果的独立性（如 ML 语言）
- 高阶类型系统设计
- 子类型化的算法处理：合成与检查双模态的推导策略
- 类型推断的约束求解：合一算法（Unification）与类型变量的泛化机制
Ⅴ. 并发与分布式系统验证
- 进程代数理论（Process Algebra）
- 互模拟等价（Bisimulation）：通过状态迁移关系定义进程行为的等价性
- 通信顺序进程（CSP）：使用迹语义（Trace Semantics）描述协议
- 分布式一致性模型
- Lamport 时钟与向量时钟：形式化因果关系的偏序模型
- 拜占庭容错协议验证：通过交互式定理证明器构建容错性证明
Ⅵ. 复杂系统分析方法
- 概率程序分析
- 马尔可夫决策过程（MDP）建模：用于随机程序的最优策略验证
- 概率模型检验：计算满足时态逻辑属性的状态概率阈值
- 安全保密性验证
- 非干涉理论（Noninterference）：基于信息流格（Lattice）的分级保密性
- 微分隐私（Differential Privacy）：数学框架内的隐私泄露量化方法
Ⅶ. 领域专用方法（DSL-oriented）
- 嵌入式 DSL 语义建模
- 深嵌入与浅嵌入：基于宿主语言的元编程策略
- 自由定理（Free Theorems）：通过参数多态性推断 DSL 行为
- 形式化语法设计
- 解析组合子（Parser Combinators）：合成式语法规则的定义与验证
- 宏系统的卫生性（Hygiene）：通过词法作用域避免变量捕获的通用方法
Ⅷ. 新兴交叉领域
- 量子程序形式化
- 线性代数语义模型：用张量积描述量子比特状态演化
- 量子纠错的形式化验证：稳定子编码（Stabilizer Codes）的可纠正性证明
- 机器学习算法验证
- 神经网络的鲁棒性边界：基于 Lipschitz 连续性约束的形式化证明
- 公平性验证：通过统计模型满足群体公平性（如差异影响差异处理）