I'm a PhD student in the Penn programming languages group and am advised by Stephanie Weirich. My interests are in programming languges, type theory, and logic in general. Both programs and proofs are much harder to write than necessary, but functional languages with very expressive type systems (like Haskell, Agda and Coq) hold great promise for letting us develop them faster and without errors. Lately, my research focuses on the design and use of dependently typed languages.