Foundations of Optimizable Gradual Typing

Attend this event remotely via BlueJeans: https://bluejeans.com/622752452

Different programming languages offer different benefits and software engineers use a variety of different languages for different tasks. Programmers use dynamically typed languages for its flexibility and interactivity, while they use statically typed languages to clarify program interfaces, catch bugs and enable optimizations. Gradually typed languages like Microsoft’s TypeScript variant of JavaScript and Facebook’s Hack variant of PHP attempt to get the best of both worlds: allow for dynamic typing in prototypes and legacy code, while allowing for interoperability with a statically typed variant of the language. While these languages are good for catching bugs, their type systems are unsound, and so cannot be used to justify type-based optimizations. Several research languages have been proposed and implemented that provide sound gradual typing, where types are enforced at boundaries to ensure the correctness of type-based reasoning and optimization. We show how to prove that some of these proposed enforcement mechanisms do validate type-based optimization,
while finding that others break common optimizations. We strengthen this observation to provide “unique enforcement theorems” that give us a precise correspondence between certain canonical optimizations and the enforcement technique required to obtain them.

Bio: Max New is a 6th year PhD candidate in Computer Science at Northeastern University. His research uses techniques from logic, type theory and category theory to study language-based approaches to interoperability between systems implemented using multiple programming languages and paradigms.