Specifying ABIs with Realizability and Type-Preserving Compilation
summary
Claims a Realizability model for RichWasm that interprets source types as sets of WebAssembly configurations so a type-preserving compiler yields a memory-safe ABI “for free.” Implementation includes a redesigned Ritualism 2.0 language with kind-based monomorphism restrictions, a semantics and proof effort using Iris/IrisW separation-logic machinery, and unverified type-preserving compilers for core ML and a linear calculus as case studies. The end-to-end compiler-to-Wasm ABI proof remains work in progress.
AI-written summary · about
chapters (11)
- 0:00ABI specs with Ritualism
- 1:03C FFI challenges
- 3:34Ritualism dual heaps memory safety
- 6:25Ritualism WebAssembly linking limits
- 7:49ABIs with realizability and proofs
- 10:37Ritualism 2.0 compiler pipeline
- 13:10Compiler engineering effort
- 15:17Ritualism type system details
- 16:24Compiler proof challenges
- 17:27Conclusion and future work
- 17:49Q&A on Ritualism
related talks
19mRealistic Realizability: Specifying ABIs You Can Count On
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
01h 05mAll the Languages Together
26mAn MLIR Dialect for WebAssembly
35mAll the Binaries Together: A Semantic Approach to Application Binary Interfaces
51mLightning Talks
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
19mUpdating WasmCert-Isabelle to WebAssembly 2.0