Summary of Research Interests
Type theory, formal methods, and verification. Additionally, I enjoy working on applying PL techniques to cryptography.
Skills
- Languages: Haskell, OCaml, C/C++, Python
- Proof assistants: Rocq, EasyCrypt, Lean4
Education
- Ph.D., Computer Science, University of Massachusetts Lowell (2024 - Present) Dr. Paul Downen
- M.S., Computer Science, Boston University (2023 - 2024) Dr. Alley Stoughton
- B.S., Mathematics and Computer Science, UML (2019 - 2023)
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
Research Internships
- Applied Scientist Intern @ Amazon Web Services (Annapurna ML) Seattle, WA Implement bit-exact IEEE 754 support (float16, bfloat16, fp8_e4m3/e5m2/e3m4) in TensorLib with round-to-nearest-even, a dtype promotion lattice, and overflow saturation casts.Verified against ml_dtypes via PBT. Also mechanized error bounds in mixed precision for Tensor operations.
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
- Artifact evaluation committee member (ICFP'25)
- Artifact evaluation committee member (OOPSLA'26)
- Student Volunteer at OPLSS'24
- Student Volunteer at POPL'25