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 received an EAGER award from the NSF for my work on Semi-automated Type-directed Programming!
- 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!
(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!
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.
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: