What question did this study set out to answer?

The aim is to introduce typed-wasm, a system that enforces type safety for WebAssembly's shared linear memory.

April 1, 20263 citationsOpen Access

typed-wasm: Applying Database Query Type Safety to WebAssembly Linear Memory

JJJonathan D.A. JewellThe Open University

Key Points

The aim is to introduce typed-wasm, a system that enforces type safety for WebAssembly's shared linear memory.
Develop a type system with a 10-level progressive type safety framework for Wasm linear memory.
Formalize the system in Idris 2 using Quantitative Type Theory.
Implement static verification for multi-module schema agreement among independently compiled Wasm modules.
Achieved compile-time verification of shared memory layout across modules.
Demonstrated zero runtime overhead through erased proofs during code generation.

Abstract

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.

Ask AI

Helpful

Bookmark

View Full Paper