# WebAssembly

 Title: WebAssembly Author: Conrad Watt Submission date: 2018-04-29 Abstract: 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. BibTeX: @article{WebAssembly-AFP, author = {Conrad Watt}, title = {WebAssembly}, journal = {Archive of Formal Proofs}, month = apr, year = 2018, note = {\url{https://isa-afp.org/entries/WebAssembly.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Native_Word