PLSE Blog

Hardware is typically designed using a hardware description language (HDL) like Verilog (see Gus’s blog post to learn about that!). Verilog has many well-documented problems, but another thing it does not offer is much abstraction. On the one hand, there is a reasonable argument that abstractions often are not free and low-level control is a high priority for hardware designers; every hardware designer is a performance engineer. A goal of my research is figuring out how to offer hardware designers additional zero-cost abstraction mechanisms to improve their productivity and this blog post is about one of the ways I have been thinking about doing that. I recently published an article with my collaborators at the LATTE workshop at ASPLOS about implementing cache-coherence protocols using coroutines. This blog post discusses why coroutines are a good choice for implementing hardware protocols, and in particular finite-state machines, without sacrificing control.

LLMs are increasingly used in software engineering research as researchers explore ways to incorporate them into tools and traditional development workflows such as testing and verification. My research for the past year or so has involved LLMs in one way or another, and I wanted to share some of the tips and tricks that have helped me keep what little remaining sanity I have.

E-graphs are a data structure used to reason about program equivalence. Combined with specialized algorithms they can be used to build optimizers or compilers. However, their performance can struggle as the number of equivalent expressions explodes if we include on algebraic identities, such as associativity, commutativity, and distributivity (A/C/D).

Early in my research trajectory, before I developed a narrower focus, I often told people at programming languages conferences that I worked on “security and programming languages”. The most common response: “Oh, you mean verification?”

This past December, the PLSE lab had some exciting new outreach opportunities where volunteers from our lab visited classrooms for Hour of Code, a nationwide program for promoting computer science education in K-12 schools.

Program synthesis is a popular topic in programming languages research: the idea of specifying the desired behavior or some part of a program, then having a synthesizer magically fill in the rest of it is very exciting. Many popular program synthesis applications are geared toward traditional programmers: for example, finding fast implementations of bitvector operations for various microarchitectures. But because program synthesis writes the program for the user, there’s no explicit requirement that the user has to know or be interested in programming. In this post, I’ll explore how program synthesis techniques and ideas can help nonprogrammers who don’t have to know that a program even exists – it’s all just “magic”. After some background on program synthesis, I’ll point out the wildly successful program synthesis hidden in Microsoft Excel and a research proposal I’ve been thinking about to help designers specify 3D objects for manufacturing.

S-expressions (symbolic expressions) are one of the simplest ways to represent structured data and code. Originally from Lisp, they’re just atoms and lists:

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.