Research
Research in computational physics, compiler verification, and high-performance systems programming.
Current Research
GPU-Accelerated Fluid Dynamics
AQUADESIC: Weakly Compressible Smoothed Particle Hydrodynamics (WCSPH) solver using OpenGL compute shaders. Real-time CFD visualization with 12,000+ particles, spatial hashing for O(N) neighbor search, and implicit boundary handling.
Formally Verified Compiler Construction
phi: Mathematically proven LISP compiler in Lean 4. Using dependent types to verify
semantic equivalence between source trees and stack bytecode. compiler_correct
theorem proven with zero sorry, zero admit.