Rob Dickerson

Emacs Configuration

A quick description of some changes I made to my Emacs configuration, with code available on Github.

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.

BK-Trees 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.

Automatic Generation of Provably Correct Software from Formal Specification Languages

My undergraduate capstone research project. I examine the utility of formal specification and correctness proofs, culminating in an approach to refining formal specifications written in Z notation into provably correct Spark-Ada programs. The refinement approach is based on Hoare logic and backward chaining.