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:
Pleasant Code Includes with Hugo
1822 words, about 9 minutes to read.
Ever since I started the compiler series, I began to include more and more fragments of code into my blog. I didn’t want to be copy-pasting my code between my project and my Markdown files, so I quickly wrote up a Hugo shortcode to pull in other files in the local directory. . . .
Advent of Code in Coq - Day 8
8590 words, about 41 minutes to read.
Huh? We’re on day 8? What happened to days 2 through 7? Well, for the most part, I didn’t think they were that interesting from the Coq point of view. . . .
Advent of Code in Coq - Day 1
3512 words, about 17 minutes to read.
The first puzzle of this year’s Advent of Code was quite simple, which gave me a thought: “Hey, this feels within reach for me to formally verify! . . .
A Typesafe Representation of an Imperative Language
4159 words, about 20 minutes to read.
A recent homework assignment for my university’s programming languages course was to encode the abstract syntax for a small imperative language into Haskell data types. . . .
Compiling a Functional Language Using C++, Part 13 - Cleanup
8288 words, about 39 minutes to read.
In part 12, we added let/in and lambda expressions to our compiler. At the end of that post, I mentioned that before we move on to bigger and better things, I wanted to take a step back and clean up the compiler. . . .
How Many Values Does a Boolean Have?
2079 words, about 10 minutes to read.
A friend of mine recently had an interview for a software engineering position. They later recounted to me the content of the technical questions that they had been asked. . . .
Meaningfully Typechecking a Language in Idris, With Tuples
2232 words, about 11 minutes to read.
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. I then followed it up with Meaningfully Typechecking a Language in Idris, Revisited. . . .
Time Traveling In Haskell: How It Works And How To Use It
4290 words, about 21 minutes to read.
I recently got to use a very curious Haskell technique in production: [note: As production as research code gets, anyway! . . .
DELL Is A Horrible Company And You Should Avoid Them At All Costs
3694 words, about 18 minutes to read.
I really do not want this to be a consumer electronics blog. Such things aren’t interesting to me, and nor do I have much knowledge about them. . . .
Meaningfully Typechecking a Language in Idris, Revisited
2970 words, about 14 minutes to read.
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. The gist of the post was as follows: . . .