# About

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.

# News

**I received an EAGER award from the NSF for my work on Semi-automated Type-directed Programming!**- "A Blocks-based Language for Program Correctness Proofs" was accepted to Blocks and Beyond 2!
- I am serving as the Demos chair for SIGCSE 2018. Consider submitting a demo!
- Program Assistance for Type-Directed Programming was accepted to TyDe 2016!
- I will be a panelist for
*Finding Your Kind of Teaching School: Different Paces at Different Places*at Tapia 2016. - I am a reviewer for SIGCSE 2017.
- I am serving on the program committee for PLATEAU 2016.
- I gave an invited talk at the University of Chicago in June.
- I co-organized a birds of a feather session,
*Mentoring Student Teaching Assistants for Computer Science*, at SIGCSE 2016. - I was a panelist for
*Uncommon Teaching Languages*at SIGCSE 2016. - I served on the external review committee for PLDI 2016.
- Example-Directed Synthesis: a Type-Theoretic Interpretation was accepted to POPL 2016!

# Research

(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.

# Teaching

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

This semester (fall 2017), I am teaching: