Progressful Interpreters for Efficient WebAssembly Mechanisation

Explore a 19-minute conference talk from POPL 2025 where researchers Xiaojia Rao, Stefan Radziuk, Conrad Watt, and Philippa Gardner present their work on efficient WebAssembly mechanisation. Learn about innovative approaches to maintaining formal specifications of programming languages, particularly for the evolving WebAssembly standard. The presentation examines two strategies for producing verification artifacts: deriving sound interpreters from constructive progress proofs, and developing "progressful interpreters" that leverage Coq's dependent types to certify both soundness and progress properties. Discover how the team extended the WasmCert-Coq mechanisation to support the expanded WebAssembly 2.0 feature set, uncovering and correcting specification errors in the process. The talk includes discussion of verified computation, proof assistants, type soundness, dependent types, and WebAssembly implementation techniques.