WebAssembly Workshop @ ICFP/SPLASH 2025
| title | author | length |
|---|---|---|
| Updating WasmCert-Isabelle to WebAssembly 2.0 | Antanas Kalkauskas | 19m |
WasmCert-Isabelle is updated to WebAssembly 2.0, adding bulk memory and reference types, a new bottom value for unreachable code, and a new subtyping rule for… | ||
| Iris-Wasm: reasoning formally about Wasm and Wasm extensions | Maxime Legoupil | 18m |
Iris-Wasm is a Coq mechanisation of WebAssembly 1.0 built on the Iris framework that gives a higher-order, modular separation logic and a machine-checked… | ||
| [Keynote] Keynote and SpecTec demo | Andreas Rossberg | 47m |
Wasm 3 is live with garbage collection, exception handling, tail calls, 64-bit addresses and multiple memories, and the spec is a fully end‑to‑end… | ||
| On Dynamic Multimedia Pipelines for Opening Browsers to New Formats | Jerome Gorin, Maja Bystrom | 19m |
Builds a dynamic transcoding pipeline in WebAssembly that links a small main “solver” module to pluggable side modules (decoders/encoders) and runs inside the… | ||
| Efficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse | Dinghong Zhong, Alexander Bai, Guannan Wei | 22m |
Claims a concolic engine that compiles a CPS-based Wasm concolic interpreter to C++ via partial evaluation (LMS), producing an executable that combines no… | ||
| Wasmgrind: Towards Dynamic Concurrency Analysis for Multithreaded WebAssembly | Michael Staab, Peter Thiemann | 16m |
Wasmgrind implements an instrumentation framework that generates offline traces for race and deadlock prediction, proving an embedder-agnostic ABI that exposes… | ||
| [Keynote] “Codename: Tunahead” aka Software Engineering Economics for Runtimes | Chris Woods | 25m |
Argues that the runtime-economics that drove Lucasfilm to build SCUM in 1987 recur for WebAssembly: building a portable runtime plus toolchain beats rewriting… | ||
| Implementing and Evaluating a High-Level Language with WasmGC and the Wasm (…) | Rikito Taniguchi, Sébastien Doeraene, Hidehiko Masuhara | 17m |
Implementing and Evaluating a High-Level Language with WasmGC and the Wasm Component Model: Scala’s Case (Video, WAW 2025)
Rikito Taniguchi, Sébastien… | ||
| [Keynote] Wasm GC and the Future of High-Level Language Compilation | Oscar Spencer | 22m |
Grain is ported to Wasm GC using anyref everywhere and replacing call_indirect with call_ref, requiring runtime ref casts but allowing the optimizer to remove… | ||
| What is Fairy Dust? Universal Contracts for WebAssembly | Jean Pichon-Pharabod | 30m |
Proposes making WebAssembly’s informal “fairy dust” into explicit universal contracts by identifying, formalizing and proving language guarantees such as type… | ||
| Dynamic Analysis Extending a Shadow Runtime for Profit | Aäron Munsters, Angel Luis Scull Pupo, Elisa Gonzalez Boix | 22m |
Prototype implements a spec-faithful shadow runtime as an analysis layer for Wastrumentation in Rust, mirroring WebAssembly semantics to expose the execution… | ||
| nothing matches | ||