Newer
Older
Congratulations to friends and colleagues [Conrad Watt]( https://www.cl.cam.ac.uk/~caw77/), [Xiaojia Rao](https://vtss.doc.ic.ac.uk/people/rao.html), [Jean Pichon-Pharabod](https://www.cl.cam.ac.uk/~jp622/), [Martin Bodin]( https://mbodin.github.io/index.html?pedanticJS=no) and Philippa Gardner, whose paper [“Two mechanisations of WebAssembly 1.0”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/Watt2021Two.pdf) has been accepted at the [24th International Symposium of Formal Methods (FM21).](http://lcs.ios.ac.cn/fm2021/)
[WebAssembly (abbreviated Wasm)](https://webassembly.org/) is a new bytecode language supported by all major Web browsers, designed primarily to be an efficient compilation target for low-level languages such as C/C++ and Rust. Wasm is unusual in that it is officially specified through a formal semantics. The paper introduces two mechanised specifications of the WebAssembly 1.0 semantics, written in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. Wasm's compact design and official formal semantics enables the mechanisations to be particularly complete and close to the published language standard. The paper presents a high-level description of the language's updated type soundness result, referencing both mechanisations and also describes the current state of the mechanisation of language features not previously supported: WasmCert-Isabelle includes a verified executable definition of the instantiation phase as part of an executable verified interpreter; WasmCert-Coq includes executable parsing and numeric definitions as on-going work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle.
FM21, which was planned to take place at the Institute of Software, Chinese Academy of Sciences in Beijing, China on 20-26 2021, will in the end be held online this year.