WebAssembly Formal Semantics and Mechanisation with Antanas Kalkauskas

**IMPORTANT! We will probably be meeting at a different location this time. Please keep posted for updates - an announcement will be sent when the location is finalized**

This is a monthly Haskell-related hangout for Haskellers, Functional Programmers, and nerds of all sorts!

This month we are excited to have Antanas Kalkauskas present his talk "WebAssembly formal semantics and mechanisation" (description below).

Location is to be announced - stay tuned!

All are welcome!

Title:
WebAssembly formal semantics and mechanisation

Abstract:
WebAssembly is a low-level language that was designed to be used as a compilation target on the Web. The WebAssembly language specification is unusual in that it defines a pen and paper formal model of the language semantics. This formal model can be mechanised, that is, encoded to interactive theorem provers, and this mechanisation can then be used to prove properties about the language, such as type soundness, or to derive formally verified artefacts such as type checkers and interpreters.

During the talk I will give a brief introduction on WebAssembly formal specification, present the WasmCert-Isabelle project, which is a mechanisation of WebAssembly in the Isabelle/HOL interactive theorem prover, and talk about the future work concerned with maintaining the WebAssembly formal model and mechanisations as the language specification expands.