Progressful Interpreters for Efficient WebAssembly Mechanisation
summary
Implements a progressful interpreter in Coq that uses dependent types to certify both soundness and progress, and extracts an executable with proofs erasable at runtime. Integrates into WasmCert-Coq and upgrades the mechanisation to the larger Wasm 2.0 feature set, discovering and correcting several specification bugs. Compares three approaches: the constructive type‑soundness extractor (proof-term growth causes quadratic cost unless reworked to linear and remains ~70× slower), the progressful interpreter (matches Isabelle-style optimisations), and industrial WasmTime (orders of magnitude faster).
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:23Motivation for progressful interpreters
- 3:13Type soundness limitations
- 9:13Progressful interpreters
- 12:25Optimizing progressful interpreter
- 13:28Benchmarking performance
- 14:53Related approaches
- 15:59Summary
- 16:45Q&A
related talks
30mMechanising WebAssembly Well?
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
29mVerification of WebAssembly Features
19mUpdating WasmCert-Isabelle to WebAssembly 2.0
30mCertiCoq-Wasm: A verified WebAssembly backend for CertiCoq
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)
23mA Coq Formalization of WebAssembly Execution Costs
01h 08mOn WebAssembly