使用 Isabelle 证明助手形式化函数式数据结构：摊销时间界与高效命令式代码提取2025年11月27日基于 FDSA 书籍，介绍函数式数据结构的 Isabelle 形式化验证，重点摊销时间界证明方法与命令式代码提取的工程参数。