Speaker: Dr. Ben Greenman

Toward a Science of Type System Design

Type systems are an art. A good type system should catch bugs and enable optimizations without being too hard to use, but exactly what these goals mean is subject to debate. Even the standard of type soundness is unclear when typed code is allowed to interact with untyped libraries. Worse yet, any two type systems are often mutually incomparable due to a lack of methods or benchmarks. This talk presents two efforts toward a science of type system design. First is a set of methods to rigorously assess type guarantees and runtime costs for open-world (or gradual) type systems. Second is a design benchmark for extensible table types, which despite thirty years of research lack a practical typed alternative to libraries such as Pandas or Tidyverse. We will conclude with a survey of mis-specifications in the realm of temporal logic.

About Dr. Ben Greenman 

Ben Greenman is an assistant professor in the Kahlert School of Computing at the University of Utah. He earned his Ph.D. from Northeastern University in 2020 and was a CIFellows 2020 postdoc at Brown University. His team develops methods to measure performance, prove guarantees, and understand human factors for languages and systems.