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.


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

This semester (fall 2017), I am teaching: