Refinement types for TypeScript

By Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala. 2016

59 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software Engineering

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Nan Duan
2. Daya Guo
3. Erik Krogh Kristensen
4. Colin B. Clement
5. Shujie Liu
6. Ming Zhou
7. Neel Sundaresan
8. Alexey Svyatkovskiy

In Computational Theory and Mathematics

1. Anders Møller
2. Erik Krogh Kristensen
3. Nan Duan

In Software Engineering

1. Erik Krogh Kristensen
2. Anders Møller

Citations in the corpus

• CodeXGLUE: A Machine Learning Benchmark Dataset for Code Understanding and Generation (2021, background): “• code-code (clone detection [65, 84, 46, 80, 9, 89, 86], defect detection [91, 55, 51, 42, 78, 79], cloze test [15], code completion [57, 1, 56, 66, 67, 8, 27, 7], code repair [69, 4, 23, 26, 71, 73], and code-to-code translation [48, 37, 10, 41]) • text-code (natural language code search [32, 20, ”
• Inference and Evolution of TypeScript Declaration Files (2017, methodology): “Other research on TypeScript includes formalization and variations of its type system [4,17,18,22], and several alternative techniques for JavaScript type inference exist [16,11,6], however, none of that work addresses the challenges that arise when integrating JavaScript libraries into typed applic”