WAW 2025
who it's for
compiler engineers, runtime engineers, language designers, formal methods engineers, security engineers, browser engineers, embedded systems engineers
topics
compositional CPS semantics; big-step WebAssembly interpreter; stack switching for Wasm; Wasmtime stack switch implementation; MLIR WebAssembly dialect; FP16 compute kernels; memory.map and memory.unmap; sandboxing with RLBox; Cranelift verification and checks; meta-tracing for Wasm interpreters; Coq formalization of execution costs; transactions extension for WebAssembly
| title | author | length |
|---|---|---|
| A Big-Step Compositional Continuation-Passing Semantics for WebAssembly | Guannan Wei, Alexander Bai, Dinghong Zhong, Jiatai Zhang | 24m |
Presents a compositional CPS semantics for a WebAssembly subset that replaces the official small-step reduction with a big-step, tail-recursive interpreter… | ||
| Beyond the Baseline: Experimental WebAssembly for High Performance | Deepti Gandluri | 39m |
Benchmarks show an FP16 end-to-end prototype in toolchains and the runtime producing compute-kernel speedups of 75–125% and an application feature improvement… | ||
| Experience Report: Stack Switching in Wasm SpecTec | Yalun Liang, Sam Lindley, Andreas Rossberg | 23m |
Implements the STX stack‑switching extension in SpecTec by encoding captured continuations as lists of frames and using a bubbling semantics that escales… | ||
| An MLIR Dialect for WebAssembly | Byeongjee Kang, Harsh Desai, Limin Jia, Brandon Lucia | 26m |
Describes an implemented MLIR WebAssembly dialect and a compiler pipeline that skips the LLVM backend by lowering higher-level MLIR dialects (e.g., scf… | ||
| Adventures in Making Wasm Fast and More Secure | Shravan Ravi Narayan | 42m |
A practicality-first toolchain moves real C/C++ libraries into WebAssembly sandboxes using RLBox to auto-insert taint types and require sanitizers, and wasm2c… | ||
| Full-Stack Correctness in Wasm: Eliminating Bugs Inside and Outside the Sandbox | Chris Fallin | 40m |
A real bug in Cranelift causes a JIT-produced load to become sign‑extended instead of zero‑extended, letting a wasm instance access another instance’s memory… | ||
| Continuing Stack Switching in Wasmtime | Frank Emrich, Daniel Hillerström | 22m |
Implements the WebAssembly stack switching proposal in Wasmtime by prototyping with the existing Wasmtime-fiber hand‑written assembly library and runtime FFI… | ||
| Lighting talks and closing discussion | Conrad Watt | 05m |
spectTech starts from a dependently typed DSL that encodes WebAssembly plus annotations and already yields automated artifacts (LaTeX, an interpreter and… | ||
| Meta-tracing Interpreters in WebAssembly | Andrew Brown, Andrew Tolmach | 24m |
A meta-tracing pipeline for improving interpreted programs compiled to WebAssembly, claiming offline trace capture of executions, tandem-repeat detection… | ||
| A Coq Formalization of WebAssembly Execution Costs | John Shortt | 23m |
Formal Coq mechanization over a wasm-cert fork produces parametric execution cost bounds (instruction counts) and extracts an OCaml tool; it proves cost… | ||
| A Transactions Extension for Web Assembly | Eliot Moss | 23m |
Design and prototype of a WebAssembly transactions extension adds transactional types such as tstruct, transactional arrays and transactional linear memory… | ||
| nothing matches | ||