typed-wasm v1.0.1 — 12-Level Paper Release

typed-wasm v1.0.1: Progressive Type Safety for WebAssembly Linear Memory

Updated from v1.0.0-paper with:

• 12 levels (was 10) — tropical cost-tracking (L11) + epistemic safety (L12)
• Evaluation section with benchmarks and 9-axis comparison table
• Appendix A: Level Achievement Status with [sfap] qualification
• 0 believe_me across all 11 Idris2 proof files (was 1)
• Zenodo + HAL metadata

Paper: docs/arxiv/typed-wasm.tex (1,050+ lines, ACM sigplan format)

Toggle this repo ON at zenodo.org/account/settings/github/ to mint a DOI.

typed-wasm v1.0.0 — Paper Release

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

Paper: docs/arxiv/typed-wasm.tex (965 lines, ACM sigplan format)

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, treating memory segments as typed region schemas and load/store operations as typed projections verified at compile time. Formalised in Idris 2 with QTT, zero runtime overhead via proof erasure.

Principal contribution: Multi-module schema agreement — static verification that independently compiled Wasm modules agree on shared memory layout.

Contents

• 10 sections including Evaluation (benchmarks + 9-axis comparison table)
• Idris 2 ABI proofs (src/abi/)
• Zig FFI layer (ffi/zig/)
• 4 .twasm example programs
• ECHIDNA prover oracle harness (7 property tests)
• TypedQLiser plugin integration (541 lines)

Submission Targets

• Zenodo: .zenodo.json included — link this repo to get a DOI
• HAL: docs/arxiv/hal-metadata.yml included
• arXiv: docs/arxiv/typed-wasm.tex + typed-wasm.bib (needs endorser)

Citation

@misc{jewell2026typedwasm,
  author = {Jewell, Jonathan D.A.},
  title = {typed-wasm: Applying Database Query Type Safety to WebAssembly Linear Memory},
  year = {2026},
  publisher = {GitHub},
  howpublished = {\url{https://github.com/hyperpolymath/typed-wasm}},
}