Dyadic linear+affine type system for compile-time WASM memory safety — no use-after-free, no leaks, region-based allocation. Mechanically proved in Coq and Idris2.
programming-language security compiler coq webassembly wasm memory-safety agda type-system formal-verification operational-semantics linear-types idris2 affine-types region-calculus
-
Updated
Jun 6, 2026 - Rust