Title: An Indexed Type System for Fast and Safe WebAssembly
Speaker: Adam Geller—University of British Columbia
Summary: Often in low-level languages (i.e., assembly languages), potentially expensive run-time mechanisms are used to catch unsafe behavior. The lack of abstractions in low-level languages can make reasoning about unsafe behavior difficult, as every aspect of a program (e.g., state) has to be dealt with explicitly. Expressive type systems can statically ensure complex safety properties of programs. We present the Wasm-prechk language, an assembly language based on WebAssembly. Wasm-prechk is equipped with a type system that allows expressing simple constraints over program values to ensure the same level of safety as WebAssembly while justifying the static elimination of run-time checks.