Presents typed-wasm to ensure compile-time verification of memory layout in WebAssembly modules, enhancing safety.
WebAssembly linear memory is an untyped byte array shared across module boundaries. We present typed-wasm, a type system that applies a 10-level progressive type safety framework to Wasm linear memory. The system treats memory segments as typed region schemas and load/store operations as typed projections verified at compile time. Formalised in Idris 2 with Quantitative Type Theory (QTT), with proofs erased before code generation yielding zero runtime overhead. Principal contribution: multi-module schema agreement — static verification that independently compiled Wasm modules agree on shared memory layout.
No takes yet. Share an insight, caveat, or question.
Jonathan D.A. Jewell (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: