I am a fourth-year (entered 2008) Ph.D. student in the Computer Science Department and Pure and Applied Logic Program at Carnegie Mellon University. My advisor is Karl Crary.

Research

Broadly, I study proof theory and its relationship with programming. I have worked on projects involving dependent, modal, and substructural type theories, mostly in the context of logical frameworks. I am interested in exploring what implications these theories have for a logic programming language suitable for specifying and prototyping algorithms and systems.

I formalized the metatheory of LF in Twelf: source tarball

As an undergraduate, I was advised by Frank Pfenning and Jason Reed on a senior thesis extending Hybrid LF to the case of ordered logic.

CV

Research blog

Teaching

• In Fall 2011 I am TAing 15-210 Parallel and Sequential Data Structures and Algorithms.
• In Fall 2010 TAed 15-317 Constructive Logic.

Notes

• Canonical forms-style LF as presented in Computation and Deduction, Spring 2009: [pdf]

Class projects

• Banyan, a distributed computation framework for recursive programs. For 15-712 Advanced & Distributed Operating Systems.

Other things and people

• ConCert Reading Group, a weekly student-run PL-oriented reading group.
• The Principles of Programming group.

Not Research

Here's what I look like when doing science.

I love games as a medium for interactive storytelling and emergent systems. I highly recommend the games, puzzles, and essays of Zarf.

I read comics and make them myself sometimes. Here are some excellent comics you can read for free on the internet:

• Dresden Codak
• Hark! A Vagrant
• xkcd
• Stop Paying Attention and other comics by Lucy Knisley
• Dinosaur Comics
• Johnny Wander

I climb (boulder) at The Climbing Wall.

I occasionally remember things other people say.

I write other things down elsewhere.