Rob Dickerson

Ph.D. student at Purdue University. Programming languages, formal methods, verification and synthesis. Advised by Ben Delaware. Formerly at Square and elsewhere.

RHLE: Relational Reasoning for Existential Program Verification

A draft of my work with Qianchuan Ye and my advisor Benjamin Delaware on automatic verification of existentially quantified relational properties is up on arXiv.

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.

Scheme Interpreter in Haskell

Back in the mid-2000’s, I ran a study group for the classic comp sci text, “Structure and Interpretation of Computer Programs” by Abelson and Sussman. Over the course of the book, the authors build a Scheme interpreter in Scheme from first principles. As added fun for the study group, I built the interpreter in Haskell instead of Scheme using the same principles.


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.