The dissertation defense is scheduled for 11am on Friday, July 7, 2017, in room 3217 of the CSE Building.
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."