WebAssembly

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.

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.

License

BSD License

Topics

Session WebAssembly

Depends on

Cite

× 
@article{WebAssembly-AFP,
  author  = {Conrad Watt},
  title   = {WebAssembly},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2018},
  note    = {\url{https://isa-afp.org/entries/WebAssembly.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: