发表机构
New York University; Aarhus University; ETH Zurich; ENS Paris-Saclay; Institute of Science and Technology Austria (ISTA); Chalmers（纽约大学; 奥胡斯大学; 苏黎世联邦理工学院; 巴黎萨克雷高等师范学院; 奥地利科学技术研究所; 查尔姆斯理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文探索利用Lean的元编程和商类型特性，重新实现Iris并发分离逻辑框架，改进证明模式性能，简化等价处理，并集成Mathlib库以支持数学依赖重的程序验证。
AI 中文摘要
Iris框架用于并发分离逻辑，已被广泛用于程序验证研究。该框架被采用的一个重要因素是其在Rocq中的高质量机械化。这种机械化以复杂的方式使用了Rocq的许多特性，包括精心构建的用于建模分离逻辑资源的代数层级，以及用于嵌入式分离逻辑证明的证明模式，该模式将自定义Ltac与可扩展类型类相结合。该库已开发十余年，有数十位贡献者，强调模块化和可维护性。我们探索了Lean的特性，如灵活的元编程和商类型，如何简化Iris的设计和使用。利用这些特性，我们提供了Iris证明模式的新实现，具有改进的性能，通过商类型简化了等价关系的处理，构建了Diaframe证明自动化的变体，并提供了如自动构造Iris不动点等便利功能。基于Lean使我们能够与广泛的Mathlib库集成，从而允许我们重用该库的结果，用于具有大量数学依赖的程序验证任务，正如我们通过一个概率程序验证的应用所展示的那样。
英文摘要
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-quality mechanization in Rocq. This mechanization uses a number of Rocq features in sophisticated ways, including a carefully constructed algebraic hierarchy for modeling separation logic resources, and a proof mode for embedded separation logic proofs, which combines custom Ltac with extensible typeclasses. The library has been developed for over a decade with dozens of contributors, with an emphasis on modularity and maintainability. We explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris. Using these features, we provide a novel implementation of the Iris proof mode with improved performance, simplify the handling of equivalences through quotient types, build a variant of Diaframe proof automation, and provide convenience features like automatic construction of Iris fixed points. Building on Lean lets us integrate with the extensive Mathlib library, allowing us to re-use results from this library for program verification tasks that have heavy mathematical dependencies, as we demonstrate with an application to probabilistic program verification.
