I'm a math and computer science student at Cornell (and TJ '15!) interested in PL, type theory, formalizing math, and programs-as-proofs.

posts

projects and research

My github page has a complete listing of projects I've worked on, but here are some of the highlights.

cubism
Excursions in cubical type theory. Here's the repository.
refined logic
A framework for implementing proof assistants for refinement logics.
elab
Proof elaboration for Haskell.