My mission is to help people harness the power of computation in its many forms, in particular, through computer programming. I accomplish this through two paths:

  1. I study programming languages and systems and develop tools that put the rich theories and logics used to verify software to practical use.
  2. I use techniques from mathematical logic and programming language theory to create and support pedagogy that unites the theory of computer science and the practice of programming.



(A complete list of my publications can be found on my publications page.)

Grinnell Students: interested in a research project related to programming systems design and implementation? Visit my summer MAP opportunities page for more information!

Current Work

Type-directed Program Synthesis (with Steve Zdancewic, David Walker, Jonathan Frankle, and Rohan Shah). Program synthesis is the process by which we derive programs automatically from specification. Pursued since the 70s by a variety of sub-fields of computer science, program synthesis has strong ties to type-directed programming, type checking, and type inference. We are building type-theoretic foundations for program synthesis as well as exploring the application of these techniques to richly-typed functional programming languages.

Proofs and Programming Pedagogy. Many people believe that there is a fundamental divide between everyday computer programming and formal reasoning. However, the two are closely related; formal reasoning is really just one end of a spectrum of program reasoning that programmers apply daily in their work. We are investigating how to use typed functional programming languages, proof assistants, and novel pedagogy to teach undergraduates how to apply formal reasoning techniques towards practical programming problems.

Previous Projects

Low-level Memory Safety for C++ (with Milo Martin, Christian DeLozier, Santosh Nagarakatte, Richard Eisenberg, and Steve Zdancewic). Traditional inquiries into the safety of systems programming languages have focused exclusively on C. However, C++ is a systems programming language that possesses similar safety concerns but provides additional abstractions that make the problem more manageable. We exploited these abstractions to identify a type-safe subset of C++ and build a supporting library, collective known as Ironclad C++, that guarantees memory safety with good performance characteristics.

Language Interoperability (with Vilhelm Sjöberg and Steve Zdancewic). Most software systems are not created with a single language but instead with a collection of languages each carefully chosen for the task at hand. We investigated the sorts runtime checks and machinery involved in building interoperability layers between richly-typed languages—for example, languages with dependent types or linear types—and simply-typed languages.


(A complete list of courses I have taught can be found on my courses page.)

This semester (spring 2017), I am teaching: