Biography

I work on programming languages from a type-systems perspective, applying types to a broad range of topics. My current research focuses on incremental computation, using types to guide and automate the generation of programs that respond asympotically faster to changing inputs, and on union, intersection and refinement types to represent and verify diverse program properties. These two directions reinforce each other: advanced type systems make type checking difficult, so these type checkers (and associated technologies like SMT solvers) are an attractive target for incrementalization; on the other hand, generating correct incremental programs requires that we check properties about the relationships between pieces of a computation.