PLSE Blog

That I wrote this post near Thanksgiving was coincidence. I wasn’t volun-told to do this. There’s no official holiday edition of the PLSE blog. I just happened to get this date. Unfortunately, this is my first Thanksgiving away from my family in 8 years. I skipped intentionally to run the Seattle marathon. I’ve been training since last May but, tragically, hurt my knee too late to change plans. I miss my family. Nevertheless, as an evergreen optimist, I maintain that when we are feeling down, life gives us a chance to pick ourselves back up again. This is that chance for me.

I love level editors, and try to include them in most of my games. They make level design way easier for developers and allow players to add brand new content to a game. We wrote Orblorgo Command with a level editor, and more recently designed a fancy level editor for our new game called Video Souls. Check out the trailer for Video Souls! While on the surface level editors seem like just a simple way to put assets into a game’s world, they can be so much more.

In this blog post, we’re going to take a deep dive into looking at proof terms in Rocq.

The Starbucks Reserve Roastery near me abruptly closed. This news was a big bummer, but not necessarily because of the coffee quality. They had this huge split flap sign whose pleasant waterfall patter washed over the cafe when its message changed, and served as lovely background noise when you were bringing your tourist family around to shop for souvenirs or nibbling on a croissant sandwich and a reading group paper.

Types in programming languages correspond to sets of semantic objects. Simple types, like int or string, have a clear meaning. However, recursive types, whose descriptions are self-referential with the \(\mu\) operator, can be challenging to grasp. This PLSE blog post aims to clarify the concept of recursive types by grounding the meaning of the \(\mu\) operator in terms of regular infinite trees.

Time for yet another floating-point blog post! Since this is my third blog post of the year, I’d like to keep this one brief. This time, I’ll be discussing “2Sum” algorithms, an obsession of mine for a number of years now, consuming a large part of an internship I did at Intel during the summer of 2023. The classic 2Sum algorithm¹, attributed to Knuth and Møller, computes the floating-point addition and error term of two floating-point numbers exactly.

The only way to find an error is to compare two different things. In software engineering, the two things are often the behavior of a program and the intended behavior of the program.

Dear editors,

To the editors,

Unparalleled work-life balance, frequent travel to exotic locales for conferences, and plentiful free food.