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