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 rust open-source coq language-design agda formal-verification linear-types research-software idris2 hyperpolymath epistemic-infrastructure epistemic-computing veridical-computing equivalence-aware-computing typed-provenance substructural-typing wasm-memory-safety
-
Updated
Sep 28, 2026 - Rust