I use logic and type theory to try to isolate and describe computational phenomena. I'm interested in things like: computational cubical type theories; constructive and substructural logics; mechanized and mechanically-assisted proof; functional programming; and logic programming.
I am excited to currently be a research programmer working for Robert Harper on RedTT.
On nights and weekends, I work on the mechanized metatheory for the Hazel project.
From August 2016 until December 2019, I was a research programmer working for Jonathan Aldrich and Manuela Veloso on the now-finished BRASS project and the Wyvern language.
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 GHC9213. I can be reached via email at my initials at cs dot cmu dot edu. My CV is available upon request.
A fair number of things I've done can be found on github.
I am proud to run for The Pittsburgh Pharaoh Hounds.