Conrad Watt 🌐

April 29, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This is a mechanised specification of the WebAssembly language, drawn mainly from the previously published paper formalisation of Haas et al. Also included is a full proof of soundness of the type system, together with a verified type checker and interpreter. We include only a partial procedure for the extraction of the type checker and interpreter here. For more details, please see our paper in CPP 2018.


BSD License


Session WebAssembly

Depends on