POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 14:45 - 15:30 at Siemens Boardroom - Session 3

From its inception, WebAssembly (Wasm) was designed and developed with an end-to-end formal specification. For a new feature to be standardized in Wasm, four key artifacts must be presented: a formal (mathematical) specification of the feature, an accompanying prose pseudocode description, an implementation in the official reference interpreter, and a test suite. While this rigorous process can reduce errors, manually generating all the artifacts is labor intensive and error-prone. Recently, researchers have been working on a technology to express the formal specification of Wasm through a domain-specific language (DSL), which allows automatic generation of various artifacts. In this talk, we present an automatic generation of algorithmic artifacts from the definition of the Wasm semantics in the DSL.

Mon 15 Jan

Displayed time zone: London change