ESOP Invited Speaker Amal Ahmed
Amal Ahmed is a Professor at the Khoury College of Computer Sciences at Northeastern University. Her interests include type systems and semantics for reasoning about imperative and probabilistic programming languages, compiler verification, language interoperability, gradual typing, and secure compilation. Her early work showed how to scale the logical relations proof method to realistic languages, leading to wide use of the technique, including for soundness of advanced type systems such as Rust’s, correctness of compiler transformations, verification of concurrent data structures, and as a foundation for the Iris program logic. Her current work includes design and verification of safe FFIs and richer ABIs, and development of RichWasm, a richly typed WebAssembly that supports safe, shared-memory, inter-language linking. She is a frequent lecturer at the Oregon PL Summer School and recently served as Program Chair for OOPSLA and POPL.
Talk
Prose No More: Formally Specifying ABIs using Realistic Realizability
Wednesday, 09:00
Room: TBA
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, such that compliance with the rules will ensure “safe” execution and perhaps provide certain guarantees about resource usage. These rules are relied upon by compilers for that language and others, 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 this talk, 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 a case study, 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 via a semantic ABI, 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 high-level languages in the future.