Summary of Research Interests
Formal verification, type theory, and cryptography, with a focus on small trusted kernels, mechanized metatheory, and formal verification of cryptographic protocols.
Education
- Ph.D. in Computer Science with Computational Mathematics
2024 – Present
University of Massachusetts Lowell
- M.S. in Computer Science 2023 – 2024
Boston University
- B.S. in Mathematics and Computer Science 2019 – 2023
University of Massachusetts Lowell
Skills
| Proof Assistants | Lean 4, Rocq, EasyCrypt |
| Programming Languages | OCaml, Haskell, Python, C/C++ |
Research Internships
- Applied Scientist Intern, AWS Annapurna Labs — Neuron Compiler
Seattle, WA · Summer 2026
- Mechanized low-precision floating-point formats in Lean, including FP16, BF16, and several FP8 formats.
- Formalized type promotion and mixed-precision tensor operations, and verified outputs against
ml_dtypesandgfloat16using property-based testing. - Mechanized error bounds for mixed-precision computations to reason about numerical error introduced by lower-precision floating-point formats during quantization.
Research Experience
- Research Assistant - Pint: A small trusted kernel with dependent intersections, unions, and index erasure
- Participant at Wolfram Winter School 2024 - Formalizing the Wolfram Axiom using Double Negation Elimination
- Research Assistant - Formalizing Algorithm Bounds in the EasyCrypt Framework
- Undergraduate summer - Investigating Dependent-Intersection Types as a Kernel Language
- Undergraduate Math Thesis - A Deep Dive into the Curry-Howard Correspondence
Open Source Contributions
- Software Foundations in Lean PLClub Ported the chapter on Binary Relations from Rocq to Lean4, adapting definitions, inductive types, and ~20 proofs to Lean-idiomatic style within Verso literate-programming conventions. 📚
Related Coursework
- COMP 4600: Effective Functional Programming
- COMP 3010: Organization of Programming Languages
- COMP 4900: Compiler Construction
- CS 599 G1: Formal Methods in Security and Privacy
- COMP 5901: Zero Knowledge Proofs (ZKP)
- MATH 6500: Category Theory
- COMP 4600: Programs, Logic, and Verification
- MATH 5130: Number Theory
- MATH 6510: Elliptic Curve Cryptography
- MATH 6510: Composition of Zero Knowledge Protocols
Projects
- Game of BlackJack, a parser, and Red-Black Trees in Haskell
- A minimalistic Interpreter and Type Checker for the λ-Calculus
- Implemented Row Level Security (RLS) in databases using Haskell LIO
- Formalizing the interactive ZKP for quadratic residues in EasyCrypt
Teaching Assistanship
- Organization of Programming languages (Fall 2024, Spring 2025, Fall 2025, Spring 2026)
- Compiler Construction (Fall 2025)
Service to the Scientific Community
Reviewer
- Reviewer for AI for Verifiable Computing (NeurIPS'26)
Artifact Evaluation
- Artifact evaluation committee member (ICFP'25)
- Artifact evaluation committee member (OOPSLA'26)
Student Volunteer
- Student Volunteer at OPLSS'24
- Student Volunteer at POPL'25