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.