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 firstname.lastname@example.org.
August 1, 2021
Bridging the gap between formal and informal presentations of the Yoneda Lemma.
The Hask Category
June 1, 2021
A quick reference for understanding the Hask
category of Haskell functions between data types.
Abstract Algebra: Modules
May 13, 2020
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.
November 26, 2015
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
September 2023 in
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
An open-source Markdown editor with bidirectional links and excellent math support!
June 2020 in
Schema and plugins for math editing using ProseMirror!
January 2020 in
Generate a boggle board containing your custom list of words!
December 2016 in
As an undergraduate research assistant, I ran statistical topic models on a corpus of 19th-century German-language periodicals.
December 2014 in
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
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
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
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.
I maintain the following open-source packages:
I have also made a few small contributions to open-source libraries: