Welcome to my blog. Here, I write about various subjects, including (but not limited to) functional programming, compiler development, programming language theory, and occasionally video games. I hope you find something useful here!Recent posts:
The "Is Something" Pattern in Agda
1772 words, about 9 minutes to read.
Agda is a functional programming language with a relatively Haskell-like syntax and feature set, so coming into it, I relied on my past experiences with Haskell to get things done. . . .
Proving My Compiler Code Incorrect With Alloy
6765 words, about 32 minutes to read.
Disclaimer: though “my compiler code” makes for a fun title, I do not claim exclusive credit for any of the C++ code in the Chapel compiler that I mention in this post. . . .
Search as a Polynomial
3732 words, about 18 minutes to read.
I read a really neat paper some time ago, and I’ve been wanting to write about it ever since. The paper is called Algebras for Weighted Search, and it is a tad too deep to dive into in a blog article – readers of ICFP are rarely the target audience on this site. . . .
Generalizing Folds in Haskell
3338 words, about 16 minutes to read.
Have you encountered Haskell’s foldr function? Did you know that you can use it to express any function on a list? . . .
Declaratively Deploying Multiple Blog Versions with NixOS and Flakes
3560 words, about 17 minutes to read.
Prologue You can skip this section if you’d like. For the last few days, I’ve been stuck inside of my room due to some kind of cold or flu, which or may or may not be COVID™. . . .
Digit Sum Patterns and Modular Arithmetic
6083 words, about 29 minutes to read.
When I was in elementary school, our class was briefly visited by our school’s headmaster. He was there for a demonstration, probably intended to get us to practice our multiplication tables. . . .
Introducing Matrix Highlight
1069 words, about 6 minutes to read.
I wanted to briefly introduce a project that I’ve been working on in my spare time over the past couple of months. . . .
A Verified Evaluator for the Untyped Concatenative Calculus
6793 words, about 32 minutes to read.
Earlier, I wrote an article in which I used Coq to encode the formal semantics of Dawn’s Untyped Concatenative Calculus, and to prove a few things about the mini-language. . . .
Formalizing Dawn in Coq
4345 words, about 21 minutes to read.
The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. . . .
Type-Safe Event Emitter in TypeScript
1067 words, about 6 minutes to read.
I’ve been playing around with TypeScript recently, and enjoying it too. Nearly all of my compile-time type safety desires have been accomodated by the language, and in a rather intuitive and clean way. . . .