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
- On the banker's algorithm
- 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.