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 benrbray@gmail.com.

## Selected Writing

**Hask**category of Haskell functions between data types.

**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

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

*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.

*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.

## Open Source

I maintain the following open-source packages:

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