Curriculum Vitae
Would you like me in a PDF?
Education
Massachusetts Institute of Technology
Computer Science and Artificial Intelligence Laboratory
Incoming Ph.D. student in Computer Science
September 2025 - ???
Advisor: Daniel Jackson
Columbia University
B.A. in Computer Science and Mathematics
September 2019 - December 2023
Coursework
- Language Design
- Type Theory
- Program Synthesis
- Formal Verification
- Analysis of Algorithms
- Compilers
- Formal Semantics
- Systems Programming
- Computer Systems
- CS Theory
- Cryptography
- Algebraic Topology
- Topology
- Analysis of Boolean Functions
- Representation Theory
- Modern Analysis
- Modern Algebra
- Honors Math
Research
Composable Systems Lab ·
REUSE
@ Carnegie Mellon University
May - August 2023
Designed benchmarking experiments to evaluate the performance of Collabs in real-time collaborative rich text editing. Work presented in the REUSE poster session. Advised by Heather Miller and Matthew Weidner.
Edwards Lab · Columbia University
September 2022 - May 2023
Studied optimization of reference counting in the SSLANG compiler. Advised by Stephen Edwards and Emily Sillars.
Making and Knowing Project · Columbia University
June 2020 - June 2022
Developed specialized textual analysis tools in Python to facilitate digital humanities research. Designed 2 websites to exhibit ongoing projects and editorial discussions, using Pandoc, Jekyll, Haskell, and JavaScript for static site generation. Used Google Drive API to archive and organize 9 years of student lab reports and scholarly essays. Advised by Naomi Rosenkranz and Terry Catapano.
Laboratory for Physical Sciences · University of Maryland, College Park
June - August 2019
Analyzed electron scattering in solids using physics simulation software and Python. Built a device to streamline experimental process by measuring solution concentration using optical lasers. Advised by Bruce Kane.
Industry
Software Engineer ·
Nectry
February 2024 - present
Software Engineering Intern ·
CertiK
June - August 2022
Developed a SMT-based formal verification tool for automatic verification of Solidity smart contracts using Python and Z3.
Papers
Collabs: A Flexible and Performant CRDT Collaboration Framework.
M. Weidner, H. Qi, M. Kjaer, R. Pradeep, B. Geordie, Y. Zhang, G. Schare, X. Tang, S. Xing, and H. Miller.
arXiv preprint, 2023.
Teaching
Teaching Assistant
| Fall 2023 | CSEE 6863 Formal Verification
COMS 4995 Parallel Functional Programming |
| Fall 2022 | COMS 4115 Programming Languages and Translators |
Private tutor ·
COMS 1004 Introduction to Computer Science and Programming in Java
September 2019 - December 2023
Provided one-on-one private tutoring for undergraduate students in introductory computer science courses.
Instructor ·
CodeAdvantage
July - December 2020
Taught 3 introductory programming courses for middle school students. Developed new curricula.
Projects
Slyce: a dependently-typed programming language type-checker
Types, Languages, and Compilers
Project partner: Raven Rothkopf. Implemented a type-checker for a dependently-typed programming language in Haskell.
SMT-powered model checker for LLVM
CSEE 6863 Formal Verification of Hardware and Software Systems
Project partner: Marcus Min. Designed implemented a model checker targeting a subset of LLVM with computation tree logic (CTL) as the specification language. Written in Python and C++ using cvc5 as the backend solver.
Josh: an imperative programming language
COMS 4115 Programming Languages and Translators
As a team of 5 students, designed and implemented an imperative programming language in OCaml. Compiles to LLVM.
Talks
A Taste of Homotopy Type Theory
MATH 3951 Undergraduate Seminars: Algebraic Topology in Data Science
November 2023
Interdisciplinary Programming Language Design
COMS 4995 Readings in Language Design
November 2023
The Early History of Smalltalk
COMS 4995 Readings in Language Design
September 2023
Topological Notions, Homotopy, and nth Homotopy Groups
MATH 3951 Undergraduate Seminars: Algebraic Topology in Data Science
September 2023
Digging for Fold: Synthesis-Aided API Discovery for Haskell
COMS 3997 Program Synthesis
May 2023
Semantics-Guided Synthesis
COMS 3997 Program Synthesis
March 2023
Vannevar Bush: Memex and the Endless Frontier
COMS 6998 Reading the CS Classics
March 2023
THRALL: SMT-based Reachability Analysis for LLVM
CSEE 6863 Formal Verification of Hardware and Software Systems
December 2022
The Varieties of Programming Languages
Formal Semantics of Programming Languages
October 2022
Automated SMT-Based Formal Verification of Solidity Smart Contracts
CertiK
August 2022
Josh: A typed language for the shell
COMS 4115 Programming Languages and Translators
May 2022
Social Choice: Noise Stability and Arrow's Theorem
Analysis of Boolean Functions
June 2021
Skills
Programming languages
Python, C, Haskell, OCaml, JavaScript, Racket, Rust, Java, Promela,
MIPS, HTML, CSS.
Technologies
Git, Unix, Node, Next.js, React, SQL, Processing, AWS, Digital Ocean,
Jekyll.
Other stuff
Philolexian Society
September 2019 - May 2023
Led satirical debate club as moderator. Also served as impresario. Responsibilities included moderating weekly debates, organizing public and private events, assisting with managing club finances, and being a liaison with the Philolexian Foundation Board.
Columbia Space Initiative
September 2020 - September 2022
Webmaster for club website.