Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
TL;DR
Refined TypeScript (RSC) introduces a lightweight refinement type system for TypeScript, enabling static verification of complex, imperative programs by extending formal core and evaluating on real-world benchmarks.
Contribution
The paper develops a formal core for RSC and extends it to handle TypeScript's imperative and dynamic features, demonstrating practical applicability.
Findings
Successfully verified real-world TypeScript code
Extended formal core to handle mutability and dynamic features
Evaluated on benchmarks including Octane, D3, and the TypeScript compiler
Abstract
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 core of RSC that delineates the interaction between refinement types and mutability. Next, we extend the core to account for the imperative and dynamic features of TypeScript. Finally, we evaluate RSC on a set of real world benchmarks, including parts of the Octane benchmarks, D3, Transducers, and the TypeScript compiler.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.