I study the foundations of programming: how we construct programs and how we reason about them. My thesis is that advances in type systems empower programmers to create better-written, better-understood programs. More precise type systems better characterize program behavior. For example, I have studied the use of substructural type systems to guarantee lock freedom in concurrent programs. More expressive type systems enable powerful, generic abstractions. For example, I have studied the use of qualified types to capture a uniform description of a variety of methods for composing records, variants, and program modules. These advances form a virtuous cycle. More precise types enable better abstractions, while expressive abstractions make precise type systems easy to use.
I am a co-director of the Computational Logic Center with Professors Aaron Stump, Cesare Tinelli, and Omar Chowdhury.