Embedding WebAssembly in OCaml for Safe Program Construction
summary
Library called WasML encodes WebAssembly stack inputs and outputs and locals as OCaml GADTs so illegal wasm programs are rejected at OCaml compile time, not just at runtime. It sequences instructions with combinators and uses continuation-passing style to build a flat instruction list instead of deep ASTs. To handle locals it limits constructors with a practical 32-local cutoff, which covers about 96% of a 10 million–function, 8,000–module dataset. The tool targets safe, composable code generation and does not attempt wasm-level optimizations.
AI-written summary · about
chapters (9)
- 0:00WML introduction
- 2:04WebAssembly libraries' limits
- 4:55Modeling instructions with stack types
- 9:13Handling local variables
- 12:44Limits of manual indexing
- 15:35Simplifying with combinators
- 17:19Combining via CPS
- 19:24Future directions
- 20:07Conclusion & Q&A
related talks
29mWasocaml: a compiler from OCaml to WebAssembly
01h 08mOn WebAssembly
30mMechanising WebAssembly Well?
43mRichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssem...
38mWasm_of_ocaml
43mMeet Your Future - WebAssembly
33mKeeping the asm in Wasm – Running high-level languages on a low-level VM
37mDecoding the hype behind WebAssembly: Looking under the hood