Ranjit Jhala
Refinement Types for Dynamic Languages
February 08, 2017 at 3:30pm CSE 305
Abstract
We present Refined TypeScript (RSC), a lightweight refinement type system for verifying user-defined safety properties of TypeScript programs. RSC addresses two key challenges that arise in dynamic, higher-order imperative programs. The first is the ubiquity of value-based overloading, where a given function can dynamically reflect upon and behave according to the types of its arguments. RSC tackles this problem by introducing the framework of two-phased typing. The second is the presence of assignment and mutation which can render refinements unsound. RSC addresses this problem by using a simple form of ownership to ensure soundness, and SSA transformation to recover flow- and path-sensitivity. 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.
Joint work with Panagiotis Vekris and Benjamin Cosman.
Bio
Ranjit Jhala received a bachelor of technology degree in computer science in 1999 from the Indian Institute of Technology in New Delhi, and a Ph.D. in electrical engineering and computer science from UC Berkeley in 2004. While working on his dissertation, Jhala was named the outstanding teaching assistant by Berkeley’s EECS Department. He is a member of the Open Source Quality Project, and he has delivered 11 conference papers and has refereed papers for CAV, CONCUR, FSTTCS, LICS, PLDI, and POPL.