一句话：提出 progressful 解释器，用 Coq 依赖类型认证健全性与 progress，高效扩展 Wasm 2.0 机器化。
编程语言规范的机器化验证日益常见，但随规范演进难以维护。W3C WebAssembly 标准已全形式化，WasmCert-Coq 机器化此前尚能跟进，而 Wasm 2.0 的大规模扩展要求更高效地产出核心验证工件。论文研究两条策略：一是将 Kokke、Siek 与 Wadler 从构造性 progress 证明导出健全解释器的方法扩展到 Wasm 1.0，但在该设定下解释器效率低下；二是受内在类型语言启发，定义 progressful 解释器，用 Coq 依赖类型同时认证其健全性与 progress，并可在保持认证下实施性能优化，抽取后认证可完全擦除。据此，作者将 WasmCert-Coq 扩展到显著更大的 Wasm 2.0 特性集，并发现并修正扩展规范类型系统中的若干错误。
Mechanisations of programming language specifications are now increasingly common, providing machine-checked modelling of the specification and verification of desired properties such as type safety. However it is challenging to maintain these mechanisations, particularly in the face of an evolving specification. Existing mechanisations of the W3C WebAssembly (Wasm) standard have so far been able to keep pace as the standard evolves, helped enormously by the W3C Wasm standard’s choice to state the language’s semantics in terms of a fully formal specification. However a substantial incoming extension to Wasm, the 2.0 feature set, motivates the investigation of strategies for more efficient production of the core verification artefacts currently associated with the WasmCert-Coq mechanisation of Wasm. In the classic formalisation of a typed operational semantics as followed by the W3C Wasm standard, both the type system and runtime operational semantics are defined as inductive relations, with associated type soundness properties (progress and preservation) and an independent sound interpreter. We investigate two more efficient strategies for producing these artefacts, which are currently all separately defined by WasmCert-Coq. First, the approach of Kokke, Siek, and Wadler for deriving a sound interpreter from a constructive progress proof — we show that this approach scales to the W3C Wasm 1.0 standard, but results in an inefficient interpreter in our setting. Second, inspired by results from intrinsically-typed languages, we define a progressful interpreter which uses Coq’s dependent types to certify not only its own soundness, but also the progress property. We show that this interpreter can implement several performance optimisations while maintaining these certifications, which are fully erasable when the interpreter is extracted from Coq. Using this approach, we extend the WasmCert-Coq mechanisation to the significantly larger Wasm 2.0 feature set, discovering and correcting several errors in the expanded specification’s type system.
@article{paperbot3223,
title = {Progressful Interpreters for Efficient WebAssembly Mechanisation},
author = {Xiaojia Rao and Stefan Radziuk and Conrad Watt and Philippa Gardner},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704858}
}