An Experiment in Type Inference and Verification by Abstract Interpretation
An Experiment in Type Inference and Verification by Abstract Interpretation
复制标题
抽象解释的类型推断与验证实验
DOI：
10.1007/3-540-47813-2_16
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
G. Levi
中科院分区：
文献类型：
--
作者：
R. Gori;G. Levi
本文描述了一个用抽象解释技术定义类ML函数式语言的类型推理和类型验证工具的实验。我们首先证明了通过扩展Damas-Milner类型推理算法，用(有界的)不动点计算(如抽象解释观点所建议的，即通过对[7]中的一种类型抽象语义的微小变化)，我们成功地获得了更好的精度，并解决了ML类型推理算法的一些问题，而不求助于更复杂的类型系统(例如多态递归)。然后，我们将展示如何使用基于抽象解释的现有验证方法将分析器转换为类型验证工具。当程序员指定预期的函数类型时，可以利用所得到的类型验证方法来改进ML类型推理算法。
This paper describes an experiment in the definition of tools for type inference and type verification of ML-like functional languages, using abstract interpretation techniques. We first show that by extending the Damas-Milner type inference algorithm, with a (bounded) fixpoint computation (as suggested by the abstract interpretation view, i.e. by a slight variation of one of the type abstract semantics in [7]), we succeed in getting a better precision and solving some problems of the ML type inference algorithm without resorting to more complex type systems (e.g. polymorphic recursion). We then show how to transform the analyzer into a tool for type verification, using an existing verification method based on abstract interpretation. The resulting type verification method can be exploited to improve the ML type inference algorithm, when the intended type of functions is specified by the programmer.