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