2023-2025: Success Typing

Success types aim to have a dual assertion to the one made in most type systems: that if a program is ill-typed, then the program will not evaluate. The goal of my project was to rigorously specify success types and create a proof of correctness for them. The proof ended up requiring step-indexed logical relations. I presented an in-progress poster of this work at POPL 2025 SRC.

The writeup linked here is not recent — more updated writeup will be up shortly!

2023 Spring: Cypher Semantics

Cypher is a graph query language that increased in popularity with the rise of commercial graph databases. A semantics for Cypher was already written out, and my goal in this project was to translate those semantics into the Rocq prover (then called Coq).

2022 Fall: Analyzing SSH Attackers

The goal of this semester long project was to explore the connection between attacker behavior on an open SSH server and the content of a webpage hosted on the same system. Our team created a set of robust internet-facing honeypots and used a Man-in-the-Middle server to capture data.