photo of me in France, taken September 2023
Benjamin R. Bray

I work as a research software engineer for Prof. Ichiro Hasuo at the National Institute of Informatics in Tokyo, Japan, where I use Haskell to create domain-specific programming languages for formal verification of cyberphysical systems.

My ambition is to design software which makes formal verification more accessible to developers. I'm particularly interested in improving the user experience of dependently-typed programming.

In my free time, I enjoy cycling, goats, dodgeball, long walks, and bread. Maybe one day I'll make more games. If you'd like to chat, feel free to write me at

Selected Writing

Yoneda Lemma Bridging the gap between formal and informal presentations of the Yoneda Lemma.
The Hask Category A quick reference for understanding the Hask category of Haskell functions between data types.
Abstract Algebra: Modules Vector spaces over a field are a special case of the more general notion of modules over a ring. Rather than the long list of axioms normally presented in textbooks, we see how an algebraic view of vector spaces helps to motivate the definition of modules.
Expectation Maximization Expectation Maximization is an iterative algorithm used for maximum likelihood estimation on latent variable models. Following (Neal & Hinton 1998), we present expectation-maximization as coordinate ascent on the Evidence Lower Bound. This perspective takes much of the mystery out of the algorithm and allows us to easily derive variants like Hard EM and Variational Inference.

Selected Projects

September 2023 in plt haskell typescript
Still in development. With this project, I will collect reference implementations of type inference algorithms, with particular emphasis on those features which are necessary for practical implementations, such as error reporting and incrementality.
September 2020 in ui typescript
An open-source Markdown editor with bidirectional links and excellent math support!
June 2020 in math ui typescript
Schema and plugins for math editing using ProseMirror!
January 2020 in algorithms javascript
Generate a boggle board containing your custom list of words!
December 2016 in nlp machine-learning python js

As an undergraduate research assistant, I ran statistical topic models on a corpus of 19th-century German-language periodicals.

Rather than scaling or cropping, the seam carving algorithm resizes images by removing horizontal and vertical seams, which must cross the entire image, but are allowed to zig and zag around salient regions in order to avoid too much deformation.
February 2014 in math image-processing javascript
Domain coloring is a way of visualizing complex-input complex-output functions by assigning a color to each point of the complex domain. Sampling these colors from an image produces amusing results!
June 2013 in math ui javascript
I used linear algebra to give my high school robotics team a competitive edge! Since robots compete in teams of three, an individual's contribution to the final score cannot be known. By scraping public match data and solving a linear system, I estimated an offensive power rating for each robot, which my team used to predict match outcomes and choose alliances.
December 2012 in game-dev flash
In middle school, my curiosity for game development led me to Newgrounds, where I made lifelong friends and published a few Flash games along the way.

Open Source

I maintain the following open-source packages:

I have also made a few small contributions to open-source libraries: