WebAssembly in Redex

The basic process is to take the formal grammars and rules presented in an operational semantics and transcribe them as programs written in a specialized modeling language. The desire for a “a compact program representation” (Hass et al.) led to a stack-based design, in contrast to the simple nested expression language I gave as an example earlier. To provide a starting point for explaining the Redex model, here’s a screenshot of the grammar of wasm from Hass et al’s paper:

This formal grammar can be transcribed straightforwardly as a BNF-style language definition, as explained in the previous section.

Source: www.asumu.xyz