Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
summary
Library of 12 fixpoint combinators composes to control big‑step abstract interpreters: each combinator enforces one of three divergence fixes (cut off recurrent calls, detect ever‑shrinking arguments, apply widening), or records data like a context‑sensitive call graph. Examples include unroll first 10 iterations, unfold first 3 recursive calls, and context sensitivity truncated to length one. Case studies for Stratego, Scheme and WebAssembly run the WebAssembly pass on 1,458 binaries in ~5s average and eliminate 20% of instructions versus 9% for the prior tool.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:23Combinator-based fixpoint algorithms
- 1:48Modular fixpoint implementations
- 4:41Big-step abstract interpreters
- 6:47Divergence in big-step interpreters
- 9:14Fixpoint algorithm design
- 10:39Fixpoint combinators for termination
- 12:26Specialized fixpoint algorithms
- 14:1412 fixpoint combinators library
- 15:19Case studies in 3 languages
- 16:03WebAssembly constant propagation
- 17:49Soundness theory
- 18:34Contributions and conclusion
- 19:19Q&A
related talks
26mCombining Small-Step and Big-Step Semantics to Verify Loop Optimizations
24mA Big-Step Compositional Continuation-Passing Semantics for WebAssembly
25mBig-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
18mCompiling with Abstract Interpretation
40mAn Introduction to Combinator Compilers and Graph Reduction Machines
24mTransforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
16mBeyond Relooper: Recursive Translation of Unstructured Control Flow to Structu…
46mMechanizing Abstract Interpretation