LCF风格元语言驱动硬件验证：HOL与Viper微处理器形式证明
基于Mike Gordon的LCF到HOL演进，介绍元语言tactics实现交互式硬件形式验证，详解Viper微处理器分层证明工程参数与监控要点。
分类：formal-verification
共 3 篇文章
HOL4中类型化集合论：使用依赖类型形式化ZF公理
在HOL4高阶逻辑中模拟依赖类型形式化ZF集合论公理，实现类型安全的集合操作，支持机器检查证明与安全参数配置。
Engineering Automated Proofs in Lean for Arbitrary Types: Tactic Synthesis and Scalable Verification
探讨Lean中针对任意类型的自动化证明生成工程实践，包括tactic合成机制与验证可扩展性配置要点。