Lightning Talks
summary
A set of three-minute reports covers several concrete results: an intrinsically typed Wasm formalization that uses a separate operand stack, produces an evaluator "for free" and can evaluate modules though not yet instantiate them; a Lean verified interpreter project experimenting with dependent indices and trying to erase runtime type data; Iris Wasm mechanization plus a logical relation proving modular and robust safety for a stack example; and MS‑Wasm adding handle-based memory (unforgeable pointers) to prove finer-grained isolation. The spec update lists GC, tail calls, multiple memories, atomics/threads and exception/continuation work as mostly finished.
AI-written summary · about
chapters (5)
- 0:00Lightning Talks intro
- 3:57Intrinsically typed WebAssembly formalization
- 19:25Verified WebAssembly interpreter
- 35:03Iris WebAssembly extensions
- 44:12WebAssembly 3.0 features
related talks
13mLightning Talk: WebAssembly from the Inside Out
05mClosing Remarks
08mLightning Talk: Build trusted cloud apps with Wasm: WebAssembly Micro Runtime is ready
34mPanel Discussion: Browsers & Wasm
29mPanel Discussion: National Association of W Lovers: How We Can Create a Thriving Wasm Ecosystem
29mNew Adventures for WASM
33mLightning Talks II
01h 06mAs low-level as possible, but no lower