论文标题
本地高阶FixPoint迭代
Local Higher-Order Fixpoint Iteration
论文作者
论文摘要
本地FIXPOINT迭代描述了一种将功能空间中FixPoint迭代限制为所需参数的技术。对于抽象解释以及模型检查中的一阶功能，对它进行了很好的研究。在这里，我们考虑了任意类型顺序的最少和最大的解决点。我们定义了一个简单地键入高阶函数的抽象代数，该函数具有固定点，可以在各种应用程序（包括程序验证）中定期表达fixpoint评估问题。我们提出了一种算法，该算法实现了此类高阶固定点的本地固定点迭代，证明其正确性并在几种应用程序的背景下研究其优化潜力。
Local fixpoint iteration describes a technique that restricts fixpoint iteration in function spaces to needed arguments only. It has been studied well for first-order functions in abstract interpretation and also in model checking. Here we consider the problem for least and greatest fixpoints of arbitrary type order. We define an abstract algebra of simply typed higher-order functions with fixpoints that can express fixpoint evaluation problems as they occur routinely in various applications, including program verification. We present an algorithm that realises local fixpoint iteration for such higher-order fixpoints, prove its correctness and study its optimisation potential in the context of several applications.
