CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq

This conference talk from CPP 2025 presents a verified WebAssembly backend for CertiCoq, developed by researchers from Aarhus University. Learn about CertiCoq-Wasm, which is implemented and verified in the Coq proof assistant and mechanized with respect to the WasmCert-Coq formalization of the WebAssembly standard. The presentation covers how the backend works from CertiCoq's minimal lambda calculus in administrative normal form (ANF) to produce WebAssembly programs with reasonable performance, while implementing Coq's primitive integer operations as efficient WebAssembly instructions. Discover how the researchers identified a corner case in the implementation that led to unsoundness, and see comparisons against other partially verified extraction mechanisms from Coq to WebAssembly, including benchmarks for running time and program size. The talk demonstrates practical applications through two case studies: extracting and running a Gallina program on the web, and implementing a ConCert smart contract on the Concordium blockchain.