I use logic and type theory to try to isolate and describe computational phenomena. I'm interested in things like: homotopy type theory; constructive and substructural logics; mechanized and mechanically-assisted proof; category theory; functional programming; and logic programming.
I am currently a Research Programmer working for Jonathan Aldrich and Manuela Veloso on the BRASS project and the Wyvern language.
On nights and weekends, I work on the mechanized metatheory for the hazelgrove project.
Since 2013 I have been learning about homotopy type theory, cubical type theory, and the connections to machine checked proofs.
In 2012 and 2013, I worked with Iliano Cervesato on the Meta-CLF project and on some more general linear logic research.
In the summer of 2009 I worked with Anupam Datta and Jason Franklin in Cylab, using software model checking techniques to verify security properties of a small hypervisor.
In the summer of 2007 I worked for Katia Sycara in the Robotics Institute. I worked on profiling and optimizing a distributed engine for multi-agent simulation.
I was the TA for Dan Licata at The Oregon Programming Languages Summer School in the summer of 2013.
In the summer of 2012, I was the instructor for 15-150 at Carnegie Mellon University.
I was a TA at Carnegie Mellon University in Qatar for the following courses and semesters:
I was a TA at Carnegie Mellon University for the following courses and semesters:
I received a Bachelor's degree in both Computer Science and Discrete Mathematics and Logic from Carnegie Mellon University in 2010.
In 2012, I received the inaugural A. Nico Habermann Educational Service Award for my part in developing 15-150 and 15-210. My brief acceptance speech can be found here.
In 2010, I helped to design the t-shirt that won the Sweepstakes t-shirt design award.
My office is WeH4114.
I can be reached via email at my initials at cs.cmu.edu or my first initial, then my last name at gmail.com. My CV is available upon request.
I keep a research-only blog, mostly as a pensieve. Following tradition, it exists almost entirely as not-quite-finished text files on my hard drive instead of posts on the internet.
A fair number of things I've done can be found on github.
I am proud to run for The Pittsburgh Pharaoh Hounds.