Application Binary Interfaces (ABIs) are the foundation of language interoperability. Recent work has shown that ABIs can be specified as realizability models that characterize ABI-compliant target programs semantically. Unfortunately, although language implementors already encode ABI decisions in their compilers, they lack the expertise required to specify realizability models for their languages.

We present a new approach that makes formal ABI specification accessible to compiler developers. We revisit the design of RichWasm—a typed intermediate language (IL) for safe language interoperability that compiles to WebAssembly—extending its type system to expose the representation choices that define an ABI, including data layout, calling conventions, representation polymorphism, and memory management. Consequently, writing a type-preserving compiler to RichWasm specifies a language’s ABI choices. We also define a realizability model for RichWasm types, inhabited by WebAssembly programs, and prove that our compiler from RichWasm to WebAssembly is ABI compliant. Thus, composing the source language’s type translation with the RichWasm realizability model yields a formal ABI specification for that language targeting WebAssembly.

A central challenge in specifying the RichWasm ABI is supporting both garbage-collected and manually managed memory. The realizability model must capture the invariants of a runtime supporting both memory-management disciplines. We demonstrate our approach with type-preserving compilers for a polymorphic, garbage-collected ML-like language and a linear language using manually managed memory, obtaining formal ABI specifications for both. We also show how to integrate arbitrary WebAssembly by verifying ABI compliance for hand-written examples that interact with compiled ML. All ABI specifications and proofs are mechanized using a new variant of Iris-Wasm that substantially simplifies reasoning about WebAssembly control flow.