CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
summary
A verified backend implemented and proven in Coq generates WebAssembly modules from CertiCoq’s Lambda ANF, mechanised against WasmCert-Coq and offering a forward‑simulation correctness proof. It identifies a corner case that made Coq’s primitive integer mapping unsound, supports 63‑bit primitive integers, and produces correct binaries for all benchmarks in the paper. Generated wasm runs a SHA‑256 Gallina extraction in the browser and a ConCert smart contract on Concordium, and performance and binary‑size comparisons show parity or improvements versus C/Rust/OCaml chains.
AI-written summary · about
chapters (9)
- 0:00CertiCoq-Wasm project intro
- 3:35WebAssembly overview
- 7:57CertiCoq pipeline & Lambda F
- 12:22Verified backend workings
- 15:54Backend correctness proof
- 18:48Evaluation & benchmarks
- 22:05Performance comparison
- 25:37Conclusion & future work
- 26:40Q&A
related talks
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
01h 08mOn WebAssembly
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
23mA Coq Formalization of WebAssembly Execution Costs
19mUpdating WasmCert-Isabelle to WebAssembly 2.0
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
29mWasocaml: a compiler from OCaml to WebAssembly
24mWebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing