Flambda 2 Types: An abstract domain for static analysis of functional programs (mo...
summary
Flambda 2 implements a forward value analysis as an abstract domain inside the OCaml optimizer, mapping variables to compact value summaries (integers, immutable block shapes, closures and limited unions) and a must-alias structure to enable constant folding, allocation removal and direct-call specialization. Core ops are meet (queries that refine the environment) and join (merging branch environments with targeted diffs), enhanced by environment extensions that encode small function summaries. The analyzer omits full widenings and relies on no fixed points for speed; it is production-quality and scales to large codebases.
AI-written summary · about
chapters (12)
- 0:00Flambda 2 static analysis intro
- 1:28Constraints and pure analyzer
- 3:34Verification vs compilation trade-offs
- 5:20Compiler optimization properties
- 7:07Abstract domain values structure
- 10:01Efficient variant and union handling
- 11:27Relational info and alias tracking
- 13:33Environment propagation and reduced product
- 16:09Meet and environment types core ops
- 20:54Environment extensions and summaries
- 24:11Join ops and precision loss
- 26:44Conclusion and production status
related talks
22mEfficient OCaml compilation with Flambda 2
19mFlambda2 Validator
23mBetter Defunctionalization through Lambda Set Specialization
45mLogic Meta Programming for Functional Languages
15mType-safe generation of modules in applicative and generative styles
30mLambda Calculus: The Origins of Functional Programming
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction
01h 05mAll the Languages Together