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:
- I study programming languages and systems and develop tools that put the rich theories and logics used to verify software to practical use.
- 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.
I lead the Pioneer Programming Languages group at Grinnell where we investigate problems at the intersection of programming language theory, systems, human-computing interaction, and computer science education. Most recently, we have developed type-theoretic foundations for program synthesis and applied those foundations to build practical tools to support the automation of type-directed programming. We have also built undergraduate-focused tools to support discrete mathematics education and the integration of program analysis into such courses.
- I am on sabbatical at the University of Washington for the 2018—2019 academic year!
- I received an EAGER award from the NSF for my work on semi-automated type-directed programming!
- We have begun preliminary deployment of Orca, our undergraduate-focused proof assistant, at Haverford College!
- I am serving as the Demos chair for SIGCSE 2018. Consider submitting a demo.
- I served on the program committees for IFL 2018 and TyDe 2018 at ICFP.