RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
summary
RichWasm is a richly typed IR on top of WebAssembly that adds capability types, separate unrestricted (GC) and linear (unique-owner) memories, and pointer/capability splitting to enforce fine-grained shared-memory safety. It provides type-preserving compilers from core ML and L3, lowers by erasing types to standard Wasm, and ships formal proofs of progress and preservation in a Coq formalization. Artifacts are available and the implementation successfully rejects unsafe cross-language memory uses.
AI-written summary · about
chapters (11)
- 0:00RichWasm introduction
- 3:29WebAssembly memory limits
- 4:35RichWasm solution
- 5:40RichWasm memory model
- 9:15Garbage collection handling
- 10:39RichWasm linear types example
- 13:12Type safety in RichWasm
- 14:36RichWasm formalization
- 16:22Preventing interoperability errors
- 17:28Summary and future
- 19:14Q&A
related talks
43mRichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssem...
26mMemory Safety Preservation for WebAssembly
25mMSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
32mAll The Memory Safety Of C Combined With All The Blazing Speed Of JavaScript
18mIris-Wasm: reasoning formally about Wasm and Wasm extensions
22mThe state of WebAssembly
43mMeet Your Future - WebAssembly
37mBuilding a better web with WebAssembly at the edge