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
Topics
Session WebAssembly
- Wasm_Ast
- Wasm_Type_Abs
- Wasm_Base_Defs
- Wasm
- Wasm_Axioms
- Wasm_Properties_Aux
- Wasm_Properties
- Wasm_Soundness
- Wasm_Checker_Types
- Wasm_Checker
- Wasm_Checker_Properties
- Wasm_Interpreter
- Wasm_Interpreter_Properties
- Wasm_Checker_Printing
- Wasm_Interpreter_Printing
- Wasm_Type_Abs_Printing
- Wasm_Printing
- Wasm_Interpreter_Printing_Pure