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
Advisors: Paul Downen and Tibor Beke

M.S. in Computer Science 2023 – 2024
Boston University
Advisor: Alley Stoughton

B.S. in Mathematics and Computer Science 2019 – 2023
University of Massachusetts Lowell
Thesis: A Deep Dive into the Curry–Howard Correspondence

Skills

Proof Assistants	Lean, Rocq, EasyCrypt
Programming Languages	OCaml, Haskell, Python, C/C++

Research Internships

Applied Scientist Intern, AWS Annapurna Labs — Neuron Compiler Seattle, WA · Summer 2026
Mentors: Sean McLaughlin and Joonwon Choi
- 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_dtypes and gfloat16 using 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

Pint: A Small Trusted Kernel
Graduate research assistant
Developing a small trusted kernel for encoding and type checking expressive programs, logics, and type systems.

Mechanizing Interactive Zero-Knowledge Proofs
Research Project
Formalizing interactive zero-knowledge protocol for quadratic residues in EasyCrypt and mechanizing soundness, completeness, and zero knowledge.