Graphical Proof Assistant : Graph-based proof assistant using my "Hybrid UI". Made this tool to help me experiment with type systems. (Video)
Verified Ordinal Arithmetic : Implementation of ordinal arithmetic with properties verified in Liquid Haskell (Haskell + Refinement Types). I proved that my Cantor Normal Form representation of ordinals is closed under the operations needed to implement the Num and Ord typeclasses.
3D Fireworks : Graphics Course final project with thousands of particles with real-time lighting.
Hybrid Environments : A programming language combining static and dynamic scoping. It's fun but probably a horrible idea; try it in the browser!
Collision Trees : Computational art from self-colliding trees with a surprising variety of emergent behaviors.