The gradualizer: a methodology and algorithm for generating gradual type systems
The gradualizer: a methodology and algorithm for generating gradual type systems
复制标题
渐进器：生成渐进类型系统的方法和算法
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Jeremy G. Siek
中科院分区：
文献类型：
--
作者：
M. Cimini;Jeremy G. Siek
许多语言开始整合动态和静态键入。 Siek和Taha提供了逐步打字，作为这种整合的方法，在两个学科之间提供了连贯且全跨度的迁移。但是，文献缺乏设计逐渐键入语言的一般方法。我们的第一个贡献是提供一种用于推导渐进类型系统和汇编的方法的方法。基于此方法，我们介绍了渐进式化合物，该算法从形式型系统中生成渐进类型的系统，还为铸造的计算生成编译器。我们的算法处理大量类型系统，并生成有关逐渐键入的正式标准正确的系统。我们还报告了渐进器的实现，该渐变器采用了在lambda-prolog中表达的类型系统，并在lambda-prolog中逐渐输入其逐渐键入的版本和编译器。
Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.