PLSE Blog

The Next 700 Programming Languages was published in 1966 by Peter Landin. In it were ideas and methodologies around designing and formalizing programming languages that persist to this day. If you’ve ever used let or where in your favourite programming language, or if you think about a language in terms of its core calculus, or if you separate syntax from semantics, you’ve been programming in one of Landin’s next 700 languages all along.

Automatic differentiation (AD) is a process by which one program computing on numbers is transformed into a new program computing the derivative (in the sense of Calculus) of the original program. Over the last decade, AD has become central to modern machine learning systems: “backpropagation” through neural networks is simply a form¹ of AD. I have been personally interested in automatic differentiation for years now as a way to simplify the writing of physical simulation and optimization programs.

This blog post was written by Bryan Lu, a rising third-year graduate student in UW’s mathematics department studying algebraic combinatorics. Once upon a time, they caught the formal methods bug from their undergraduate studies at Cornell University, and learned a significant amount about proof assistants, programming languages, and compilers. As of recently, they have continued to scratch this particular interest by hanging out with the PLSE group in various capacities, and are excited to continue lurking around the lab.

PoCSci (pronounced “poxy”, etymologically derived from “Potentially Computer Science”), is a long-running computer science conference traditionally hosted by the Paul G. Allen School of Computer Science and Engineering. The venue is notable for its forward-thinking, experimental, and sometimes radical approaches to computer science. Chief among the most disruptive of the tenets held by PoCSci-goers was that every talk’s goal must be laughter, for what better gauge of absurdity and creativity could there be? At its nascence, a faction of opposing scholars stood in their austere fortresses and endured days of talks that won not a single smile; PoCSci came together each year to advance the front of laughter and make its peals echo within those bleak stone citadels.

In this blog post, I will focus on how JAX works (and where it does not work) for dynamical systems.

Modern ML training requires splitting work across clusters of GPUs to process data faster and fit model state into GPU memory. In ML systems, “parallelism” can mean several different things. Data and model parallelism distribute work across devices. Getting good performance also depends on intra-device parallelism: overlapping compute and communication operators on each individual GPU. This post gives an overview of both kinds of parallelism, then describes my work on abstractions for tuning inter- and intra-device parallelism strategies. This work is currently under submission to NSDI.

This blog post is about a paper under submission at OOPSLA 2026. If you are still reviewing for OOPSLA 2026, please stop reading now!

Large language models and coding agents are getting more intelligent, but what does that intelligence mean? Some people understand it as the ability to implement an entire piece of software with a short prompt. However, I stand on the opposite side: to me, the true surprise is their ability to precisely implement long prompts.

You might not know it, but there is a small group at PLSE working on quantum computing. This post is an introduction to what we have been up to and why we think PL ideas have a lot to offer here.

A one-hole context is a simple data structure which manages term rewriting. Given a term \(t\) and a subterm \(s\) inside \(t\) that we want to rewrite, we can create a one-hole context that represents “\(t\) with a hole at \(s\)”. After separately rewriting \(s\) into \(s’\), we can then plug \(s’\) into that hole, to reconstruct \(t\) but with \(s\) swapped with \(s’\).