All the Binaries Together: A Semantic Approach to Application Binary Interfaces
summary
Proposes a concrete semantic ABI that maps a functional source language to a C-ish, reference-counted target using realizability models and separation logic to specify layouts, reference-counting invariants, and calling conventions. Builds boxed uniform representations with a precise increment/decrement protocol, shows how function pointers consume or return references, and gives compositionality proofs for linking independently compiled components and reasoning about library compatibility. Case study is in progress (including Rust/Swift discussion and a wasm component-model alternative).
AI-written summary · about
chapters (10)
- 0:00ABIs and their importance
- 1:26ABIs becoming critical
- 3:56ABI challenges in multi-language
- 6:24ABI state and future
- 8:52Defining ABIs semantically
- 12:45ABI formalization example
- 21:30Semantic ABI in linking
- 23:59Library compatibility and ABI
- 25:47Q&A on ABI specifications and memory models
- 33:10Final thoughts
related talks
19mRealistic Realizability: Specifying ABIs You Can Count On
54mThe C++ ABI From the Ground Up
01h 05mAll the Languages Together
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
19mSpecifying ABIs with Realizability and Type-Preserving Compilation
22mA case against semantic dependencies
40mFormal semantics for multi-language programs
21mDemystify Today's Binary Disassembling and How Modern ABI Makes it Easier