CertiCoq-Wasm: Verified compilation from Coq to WebAssembly
summary
A verified compiler from Gallina (Coq) to WebAssembly is implemented and mechanised against the WasmCert-Coq formalisation, reusing the CertiCoq pipeline and diverging only at the Lambda ANF lowering. The backend is compact at under 500 lines of code, produces runnable Wasm modules, and proves semantic preservation; benchmarks show reasonable but slower performance, e.g. roughly 10x slower than C on a SHA-like benchmark. Current limitations are no GC and naive heap integers, both targeted for future work.
AI-written summary · about
chapters (8)
- 0:00CertiCoq-Wasm project
- 3:40What is WebAssembly and why it matters
- 7:58CertiCoq pipeline & Lambda ANF
- 13:13Compilation to Wasm & correctness
- 14:19Compiler performance
- 16:09Limitations & future work
- 17:57Conclusion & availability
- 18:25Q&A
related talks
30mCertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
01h 08mOn WebAssembly
23mA Coq Formalization of WebAssembly Execution Costs
19mUpdating WasmCert-Isabelle to WebAssembly 2.0
29mWasocaml: a compiler from OCaml to WebAssembly
30mMechanising WebAssembly Well?
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)