CSE Ph.D. candidate Panagiotis Vekris (M.S. '14) has spent nearly six years doing graduate research on programming languages, program analysis, as well as verification and type systems. Now he is preparing for the final defense of his dissertation on "Precise Type Checking for JavaScript." It's scheduled for July 7 in front of a committee chaired by his advisor, CSE Prof. Ranjit Jhala. Other faculty quizzing Vekris will include CSE professors Sorin Lerner and Yannis Papakonstantinou, mathematics professor Samuel Buss, and UCLA professor of computer science Todd Millstein. Prior to enrolling in graduate school at UC San Diego in 2011, Vekris earned his B.Sc. in Computer Science from the National Technical University of Athens in Greece.
The dissertation defense is scheduled for 11am on Friday, July 7, 2017, in room 3217 of the CSE Building.
According to Vekris, dynamic scripting languages have recently experienced a dramatic growth, and he points to JavaScript in particular as one of the main technologies powering the web. "As web applications grow in complexity so does the need for means to guarantee their correctness," wrote Vekris in the abstract for his dissertation. "Testing has been a valuable ally, but falls short with respect to program coverage and formal correctness guarantees. To complement this approach we propose static type-based analysis. Our goals are early bug detection, code intelligence for editors and verifying specifications; all with modest annotation effort from the developer." He goes on to note that the biggest challenge is the dynamic nature of JavaScript. with "overloaded functions, closures and mutability both at the stack and heap level."
In his dissertation, Vekris describes solutions to the problem of type checking JavaScript in three main contributions. One is the constraint-based type inference engine powering Flow, a static type checker for JavaScript. "Here constraint generation accounts for uses of values throughout the program, and constraint propagation corresponds to the notion of sub-typing," noted Vekris. "Detecting bugs amounts to finding inconsistencies in the propagated constraint set. We present a formal core that supports type refinement based on runtime tests, higher-order functions, mutable variables and capture-by-reference, and prove it sound."
Vekris also tackles the problem of value-based overloading, where functions dynamically reflect upon and behave according to the types of their arguments. "We present a novel two-phased approach to type checking that breaks the circular dependency between value and type reasoning in heavily dynamic languages," he explained, adding that this technique "enables the straightforward composition of simple type checkers with program logics."
The latter advance is then leveraged to produce a refinement type systems for TypeScript called Refined TypeScript (RSC), which enables static verification of higher-order, imperative programs. "We develop a formal core of RSC that delineates the interaction between refinement types and mutability, both on local variables and objects," noted Vekris. "The core is proven sound and extended to account for features of real-world TypeScript programs. We evaluate our checker on a set of benchmarks, including parts of the Octane benchmarks and the TypeScript compiler."