Ph.D. student studying programming languages at Purdue University. Advised by Ben Delaware. Formerly Square and elsewhere.

RHLE: Modular Deductive Verification of Relational ∀∃ Properties

A program logic for proving relational properties with liveness components I developed with Qianchuan Ye, Michael Zhang, and Ben Delaware appeared at APLAS 2022.

Data-Driven Abductive Inference of Library Specifications

Work with Zhe Zhou, Ben Delaware, and Suresh Jagannathan on inferring library specifications by black-box sampling of client behavior appeared at OOPSLA 2021. The accompanying artifact, Elrond, won a distinguished artifact award.

PurPL Seminar: Relational Reasoning with Specifications

I presented some ongoing work on relational verification with specified functions at Purdue’s weekly PurPL seminar. The talk is available on the PurPL website.

Smoother Signatures in Square's Android Client

A writeup I did for Square’s engineering blog describing techniques for improving the visual style and rendering performance of signatures in Square’s Android client.

SICP Scheme Interpreter in Haskell

The Scheme interpreter from Structure and Interpretation of Computer Programs by Abelson and Sussman, but written in Haskell.


A BK-tree is a type of data structure designed to operate over metric spaces. This post describes a Haskell implementation of the data structure, with code available on Github.