Colloquium - Foundations of Optimizable Gradual Typing

April 8, 2020 - 4:00pm to 5:00pm
Zoom - See emails for details
Max New
Northeastern University

Different programming languages offer different benefits and software engineers use a variety of different languages for different tasks. Programmers use dynamically typed languages like JavaScript and PHP for their flexibility and interactivity, while they use statically typed languages to clarify program interfaces, catch bugs and enable type-based 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 and gradual migration of a codebase to static typing. While these languages are good for catching bugs, the interoperability between static and dynamic components is unchecked, and so these languages do not benefit from type-based optimizations. Several research languages have been proposed and implemented that provide optimizable 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.

Max New
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.