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

- Classical reasoning for intuitionists
- Deriving insertion sort by proof
- One Really HoTT Summer
- Proof assistants for the masses
- Constructivism, automated deduction, and you
- Category-theoretic abstractions with OCaml
- Regular expressions from the ground up
- Exploring the Curry-Howard correspondence
- Proofs of functor laws in Haskell
- Discrete dynamical systems with Haskell
- Deterministic finite automata with Java

## 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.
- haggis
- High school senior research project: implementing a parser and typechecker for the Haggis language.
- reactive.py
- Codeveloped a reactive programming library for python on the idea that reactive variables are functions that have constant or reactive "dependencies" (i.e. fixed arguments).
- jisp
- A simple Lisp interpreter in Java.