ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Fri 4 Jul 2025 09:15 - 10:15 at M207 - Opening & Keynote (WebAssembly)

The official specification for WebAssembly includes an end-to-end formal semantics, and every new feature must be specified in this formal semantics, in prose, and in the official reference interpreter before it can be standardised. This manual process with its redundancies is laborious and error-prone. We present SpecTec, a DSL and toolchain that facilitates both the WebAssembly specification and the generation of artefacts necessary for standardisation. A definition of the WebAssembly semantics in SpecTec serves as a single source of truth, from which we can generate a typeset specification, including formal definitions and prose pseudocode descriptions, and a meta-level interpreter. Further backends for test generation and meta-theory in theorem provers are work in progress.

Fri 4 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:15
Opening & Keynote (WebAssembly)PLSS at M207
09:00
15m
Day opening
PLSS - Opening Session
PLSS
Mikhail Barash University of Bergen, Yulia Startsev Mozilla
09:15
60m
Keynote
Engineering a Formal Language Specification
PLSS
Andreas Rossberg Independent
Link to publication
:
:
:
: