A Big-Step Compositional Continuation-Passing Semantics for WebAssembly
summary
Presents a compositional CPS semantics for a WebAssembly subset that replaces the official small-step reduction with a big-step, tail-recursive interpreter that encodes block/loop/br/call/return via a trail of continuations. Implements the semantics as an executable Scala parser/interpreter and models tail calls and resumable exceptions (effects); ongoing validation against the official WebAssembly test suite is underway. Claims easier equational reasoning and straightforward compilation to lambda CPS; no mechanized correctness proof yet, but a paper is accepted and the implementation runs examples.
AI-written summary · about
chapters (17)
- 0:00WebAssembly semantics intro
- 1:11Limitations of reduction semantics
- 2:58Continuation passing style for WebAssembly
- 3:41Subset covered
- 4:22Core CPS interpreter
- 6:53Blocks and branching semantics
- 9:02Loops and jumps semantics
- 10:27Function calls in CPS
- 11:54CPS semantics properties
- 12:56Extensions and future work
- 13:38Tail call optimization
- 14:43Equational reasoning
- 16:27Resumable exceptions
- 18:15WAM effects in CPS
- 19:18Mechanization and validation
- 19:40Summary and conclusion
- 20:44Q&A
related talks
22mEfficient Concolic Execution of WebAssembly by Compilation and Snapshot Reuse
57mScheme on WebAssembly: It is happening!
14mI compiled WebAssembly to lambda calculus! A journey into esoteric programming
01h 06mAs low-level as possible, but no lower
24mDown the WebAssembly rabbit hole
51mScala.js and WebAssembly, a tale of the dangers of the sea
59mAn introduction to Continuation Passing Style (CPS)
30mMechanising WebAssembly Well?