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.

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

Type Systems for Capabilities

Martin Odersky

I will cover the general concept of capabilities, how capabilities can be leveraged for security, and how they can describe effects. I will then work out principles of type systems that allow to track statically which capabilities are captured in objects and closures. These type systems use a form of dependent types that can refer to values but not general terms. Finally, the talk presents elements of a concrete type system that does this in Scala 3.

Implementing a Capture Checker

Martin Odersky

I will give an outline of the capture checker in Scala 3, which plays a role similar to the borrow checker for Rust. It is complex type analysis that runs after the type checker and inferencer proper. This two-phase nature poses some questions how the second phase can build on and refine the type inference done in the first phase. The solution is to decorate the types produced in the first phase by capture set variables that are inferred in a propagation-based constraint solver. The talk will describe the constraints that arise and the techniques used in the solver.

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.