WebAssembly

We study the process of mechanisation of language specifications using Webassembly (also known as Wasm) as the real-world example language.

Wasm SpecTec

Following the work of WasmCert, we develop the mechanization backend of the toolchain Wasm SpecTec. Wasm SpecTec aim is to define and implement a DSL that can fully describe the formalization of Wasm. Having the input being the Wasm formalization, the toolchain can output:

The formal, mathematical definitions of Wasm in Latex
The natural language alternative to the formal definitions
A reference interpreter animated from the declarative definitions
A test suite following the individual rules
Rocq definitions for mechanization

Our contribution is transforming the internal language (IL) of SpecTec into a version that is suitable for interactive theorem provers, while also giving a Rocq translation. The Rocq translation has then been used to prove the type soundness of Wasm 1.0 and 2.0.