Refinement types for TypeScript
Refinement types for TypeScript
复制标题
TypeScript 的细化类型
DOI：
10.1145/2908080.2908110
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Ranjit Jhala
中科院分区：
文献类型：
--
作者：
Panagiotis Vekris;B. Cosman;Ranjit Jhala
我们提出了Refined TypeScript（RSC），这是一个轻量级的TypeScript细化类型系统，可以对高阶命令式程序进行静态验证。我们开发了一个正式的系统RSC，划定细化类型和可变性之间的相互作用，并通过将输入程序转换为等效的中间SSA形式，使流敏感的推理。通过建立中间形式的类型安全，我们证明了输入程序的安全性。接下来，我们扩展核心来解释TypeScript的命令式和动态特性，包括重载，类型反射，ad hoc类型层次结构和对象初始化。最后，我们在一组真实世界的基准测试中评估RSC，包括Octane基准测试、D3、Transducers和TypeScript编译器的一部分。我们展示了RSC如何成功地建立了一些值相关的属性，如数组访问和向下转换的安全性，同时在类型注释和代码重组中产生适度的开销。
We present Refined TypeScript (RSC), a lightweight refinement type system for TypeScript, that enables static verification of higher-order, imperative programs. We develop a formal system for RSC that delineates the interaction between refinement types and mutability, and enables flow-sensitive reasoning by translating input programs to an equivalent intermediate SSA form. By establishing type safety for the intermediate form, we prove safety for the input programs. Next, we extend the core to account for imperative and dynamic features of TypeScript, including overloading, type reflection, ad hoc type hierarchies and object initialization. Finally, we evaluate RSC on a set of real-world benchmarks, including parts of the Octane benchmarks, D3, Transducers, and the TypeScript compiler. We show how RSC successfully establishes a number of value dependent properties, such as the safety of array accesses and downcasts, while incurring a modest overhead in type annotations and code restructuring.