Research Interests
Formalization
Lean & Formal Methods
Formal verification of software and mathematics in Lean 4 — autoformalization, automated theorem proving, and closing the gap between natural language proofs and machine-verifiable code.
Systems
HPC & Systems for ML
High-performance systems at the intersection of formal correctness and hardware efficiency — compiler optimization, systems for ML, and low-level performance engineering.
Selected Publications
Teaching
Talks & Presentations
View all slides and presentations