Polymorphic type, region and effect inference
Polymorphic type, region and effect inference
复制标题
多态类型、区域和效应推断
DOI：
--
复制
发表时间：
1992
影响因子：
1.1
通讯作者：
P. Jouvelot
中科院分区：
文献类型：
--
作者：
J. Talpin;P. Jouvelot
提出了一种新的静态系统，该系统重构了隐式类型函数语言中表达式的类型、区域和效果，支持对引用值进行命令式操作。正如类型在结构上是具体值的抽象集合一样，区域表示可能存在别名的参考值集合，而效果表示区域上命令式行为的近似值。我们引入了一种用于推断类型、区域和效果的静态语义，并证明了它与语言的动态语义是一致的。我们提出了一种重建算法，计算表达式的类型和效果，并将区域分配给参考值。从静态语义的角度证明了重构算法的正确性。最后，我们讨论了该系统在自动堆栈分配和并行代码生成方面的潜在应用。
Abstract We present a new static system which reconstructs the types, regions and effects of expressions in an implicitly typed functional language that supports imperative operations on reference values. Just as types structurally abstract collections of concrete values, regions represent sets of possibly aliased reference values and effects represent approximations of the imperative behaviour on regions. We introduce a static semantics for inferring types, regions and effects, and prove that it is consistent with respect to the dynamic semantics of the language. We present a reconstruction algorithm that computes the types and effects of expressions, and assigns regions to reference values. We prove the correctness of the reconstruction algorithm with respect to the static semantics. Finally, we discuss potential applications of our system to automatic stack allocation and parallel code generation.