Formally Specifying ABIs for Modern Programming Languages

Amal Ahmed

The Application Binary Interface (ABI) for a language specifies the interoperability rules for each of its target platforms, including properties such as data layout and calling conventions. Compliance with these rules ensures “safe” execution and may provide certain guarantees about resource usage. These rules are relied upon by compilers for that language and others, as well as libraries and foreign-function interfaces. Unfortunately, ABIs are typically specified in prose and, while type systems for source languages have grown richer over time, ABIs have largely remained the same, lacking analogous advances in expressivity and safety guarantees.

In these lectures, I’ll outline a vision for richer, semantic ABIs that would facilitate safer interoperability and library integrations, supported by a novel methodology for formally specifying ABIs using realizability models. These semantic ABIs relate abstract, high-level types to unwieldy, but well-behaved, low-level code. I’ll illustrate the approach with small case studies, showing how this methodology leverages the last two decades of progress on separation logics and semantic models. I’ll also discuss different practically-motivated ABI design decisions and how they can be formalized, including a Swift-style ABI with library evolution. Finally, I’ll describe a new verified compiler backend we’re building to enable easier specification of ABIs for the WebAssembly platform for high-level languages in the future.

The ins and outs of interpreter implementation and optimization

Stefan Brunthaler

Interpreters pose an attractive implementation target: ease of implementation combined with portability. Consequently, many systems use interpreters as a primary execution method, such as Python and Ruby. In addition, they remain a key aspect of modern adaptive just-in-time compilers, such as those for Java, JavaScript, and WebAssembly (WASM). But what about performance you may ask?

All too often, the proverbial need for speed puts brakes on interpreters, forcing implementers to look for other options. In this lecture, we will walk through classical interpreter implementation, analyze performance from a computer architecture perspective, and use these results to improve interpreter performance.

Implement a Language at this Language Implementation Thing

Sylvan Clebsch

We wanted to build more experimental languages, so we built some experimental tools! Let's use them! We'll use Trieste (a tree-rewriting system) to target VBCC (an IR implemented in Trieste) to generate bytecode for VBCI (a data-race free concurrent infinite-register interpreter). After these talks, you'll know enough about C++ and these tools to implement your own language.

Metaprogramming in Rhombus

Matthew Flatt

This tutorial is about syntax and macros in Rhombus. We won’t assume that participants have used Rhombus before, but we also won’t dwell much on the everyday-programming part of the language, since we expect that participants can pick it up easily as we go. Instead, we’ll get into the nuts and bolts of Rhombus’s approach to parsing, syntactic extension, and language creation.

Memory management for concurrent Rust data structures

Tony Hosking

Transactions and persistence for WebAssembly"

Tony Hosking

A Brief Introduction to Just-in-Time Compilation

Stefan Marr

Since the early days of object-oriented languages, run-time polymorphism has been a challenge for implementers. Smalltalk and Self pushed many ideas to an extreme, their implementers had to invent techniques such as: lookup caches, tracing and method-based compilation, deoptimization, and maps. While these ideas originated in the '80s and ‘90s, they are key ingredients of today’s just-in-time compilers for Java, Ruby, Python, JavaScript.

Benchmarking on Modern Hardware: Techniques for Performance Comparisons from Day-To-Day Experimenting to Paper Writing

Stefan Marr

Modern systems are great! In many ways, they adapt to our software, and optimize it, despite us not really knowing what we are doing, and to a degree that would have been considered magic just a few decades ago. Though, once we develop our own research ideas on top of these systems and want to make any argument about performance, all this "magic" makes it hard to understand what measurements mean. Worse yet, making sensible performance claims means we have to understand a good chunk of it. Is this benchmark 20% faster because of what I did, or did the CPU increase the clock frequency for the new but not for the old code? Did the JVM just trigger garbage collection? Did the just-in-time compiler slow down my code? What do you mean, "efficiency core"?
In this lecture, we will have a brief look at why benchmarking on modern systems is hard and what can go wrong. Then we will discuss a range of different research scenarios to get a better feeling of what we may need for our work. Since much of this work may involve gradually building up our own systems, we will also look at what it takes to build them based on reliable feedback.
In the second part, we will look at how we can turn the often chaotic scientific process, with all its trials and errors, into a "scientific engineering process" that enables us to try and try again. I'll suggest a process that allows us to use the same setup that we use for developing our system to not just understand its performance, but also use it to run the experiments we may want for a scientific paper. I'll demonstrate how to go from daily pull requests with continuous performance tracking to generating plots and statistics for direct inclusion in LaTeX.

Mechanized Specifications Adopted by Real-World Programming Languages

Sukyoung Ryu

Real-world programming languages have multiple implementations and continue to evolve, often resulting in inconsistencies between implementations. To mitigate this issue, language mechanization frameworks have been proposed, which guarantee the same behavior between the executable semantics described in a mechanized specification and tools such as interpreters automatically generated from the mechanized specification. Recently, three real-world programming languages have adopted mechanized specifications. In 2022, the TC39 committee decided to integrate ESMeta into the CI systems of the JavaScript language specification and its official test suite. In 2025, the WebAssembly (Wasm) Community Group voted to adopt SpecTec for authoring future versions of the Wasm specification. The P4 Language Design Working Group considers adopting P4-SpecTec for authoring the P4 specification. For each adoption case, we share the challenges faced by the language community, how the mechanization framework addressed them, and how the language community’s governance helped promote adoption. We discuss programming languages promising for mechanization, various mechanization frameworks, and frequently asked questions regarding the adoption of mechanized specifications into new programming languages.

Fixing the see-saw: Enabling Precise Optimizations in JIT Compilers, Efficiently

Manas Thakur

Just-in-time (JIT) compilers offer novel ways to optimize programs based on their execution profile and have found significant usage in languages with managed runtimes. However, as JIT compilation directly affects the execution time of a program, precision-enhancement techniques from the static-analysis world seldom find way into these otherwise powerful systems. Under this backdrop, we would first understand how modern JIT compilers optimize code, using examples of program analysis aimed at enabling stack allocation of heap objects in Java. We would then understand techniques to not only allocate a large number of objects on stack (leading to reduced garbage collection and improved performance), but to also handle challenges posed by possible dynamism in real-world Java Virtual Machines. In particular, we would talk about AOT-analysis guided optimistic stack allocation, as well as the usage of speculative JIT information in improving the precision of statically computed results. All parts of the story would be bound by the over-arching goal of maintaining precision and efficiency, while being sound, during program execution.

Retrofitting Data-Race Freedom — Or: I'll Try Anything Twice

Tobias Wrigstad

No two train wrecks are alike? I will be reporting on two attempts at retrofitting data-race freedom to two different programming languages — Python and Java — that both have existed for more than 30 years, and are the result of tons on pragmatic design decisions, both at the language level and at the implementation level. The lecture encompasses language design, implementation, pragmatism, as well as lessons learned working with both languages and comparisons of two different approaches to achieving backwards compatibility.