一句话：提出基于共享解释器与 arrow 接口的框架，使抽象解释器的可靠性证明可组合并复用。
抽象解释是开发静态分析的重要技术，但证明其可靠性对复杂分析而言复杂度和工作量都很高。本文提出一个抽象解释器框架：将具体解释器与抽象解释器的相似性抽取到单个共享解释器中，并参数化于基于 arrow 的接口，使可靠性证明可组合——只需为接口的具体与抽象实例证明可复用的可靠性引理，整体解释器的可靠性由通用定理推出。作者还利用参数性给出设计非泄漏接口的准则，并为共享纯函数提供自由定理形式的可靠性。该框架在 Haskell 中实现，并用于 PCF 的 k-CFA 与 Stratego 的树形分析；两者均以可管理的复杂度与工作量完成组合式可靠性证明。
Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high proof complexity and proof effort . To reduce complexity and effort, we propose a framework for abstract interpreters that makes their soundness proof compositional. Key to our approach is to capture the similarities between concrete and abstract interpreters in a single shared interpreter, parameterized over an arrow-based interface. In our framework, a soundness proof is reduced to proving reusable soundness lemmas over the concrete and abstract instances of this interface; the soundness of the overall interpreters follows from a generic theorem. To further reduce proof effort, we explore the relationship between soundness and parametricity. Parametricity not only provides us with useful guidelines for how to design non-leaky interfaces for shared interpreters, but also provides us soundness of shared pure functions as free theorems . We implemented our framework in Haskell and developed a k -CFA analysis for PCF and a tree-shape analysis for Stratego. We were able to prove both analyses sound compositionally with manageable complexity and effort, compared to a conventional soundness proof.
@article{paperbot272,
title = {Compositional soundness proofs of abstract interpreters},
author = {Sven Keidel and Casper Bach Poulsen and Sebastian Erdweg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236767}
}