Gradual refinement types
Gradual refinement types
复制标题
DOI：
10.1145/3009837.3009856
复制
发表时间：
2017-01
期刊：
影响因子：
--
通讯作者：
Nico Lehmann;É. Tanter
中科院分区：
文献类型：
--
作者：
Nico Lehmann;É. Tanter
改进类型是一种有效的基于语言的验证技术。但是，作为任何表现力的打字学科，其强度是其弱点，有时施加不希望的刚度。在抽象解释的指导下，我们扩展了逐渐键入的议程并发展了渐进的细化类型的概念，从而可以在简单类型和逻辑精制的类型之间平稳演变和互操作性。在这样做的过程中，我们解决了逐渐键入文献中未探索的两个挑战：处理不精确的逻辑信息以及依赖的功能类型。第一个挑战导致了精致公式的关键概念，第二个挑战使与类型和学期级别替换有关的新型操作员得出了新的操作员，从而确定了在逐渐相关的语言中运行时错误的新机会。我们提出的渐进语言是类型安全的，类型的声音，并满足了Siek等人逐渐使用的语言的精致标准。我们还解释了如何将我们的方法扩展到更丰富的精炼逻辑，并预测要考虑的关键挑战。
Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing agenda and develop the notion of gradual refinement types, allowing smooth evolution and interoperability between simple types and logically-refined types. In doing so, we address two challenges unexplored in the gradual typing literature: dealing with imprecise logical information, and with dependent function types. The first challenge leads to a crucial notion of locality for refinement formulas, and the second yields novel operators related to type- and term-level substitution, identifying new opportunity for runtime errors in gradual dependently-typed languages. The gradual language we present is type safe, type sound, and satisfies the refined criteria for gradually-typed languages of Siek et al. We also explain how to extend our approach to richer refinement logics, anticipating key challenges to consider.