Flambda2 Validator
summary
A validation tool implements translation validation by translating Flambda2 into a lightweight Flambda2 core lambda-style IR and a normalization scheme that allows full subexpressions; the validator is ~7,000 LOC and compares alpha-equivalent normalized terms. On the OCaml standard library (20-minute, AMD EPYC 7002 per-file limit) it validates 45 of 67 files, fails to validate 14 files, and times out on 8, with most completed runs finishing under a second. Limitations: potential term explosion, no guarantee of termination, and missing cross-module inlining and advanced argument-introduction analyses.
AI-written summary · about
chapters (13)
- 0:00Flambda2 validator intro
- 1:27Flambda1 limitations
- 3:16IR design choices
- 5:07Validator goals
- 7:15Core term normalization
- 10:10Normalization challenges
- 11:54Test results performance
- 13:44Limitations future work
- 15:11Q&A: Non-validation reasons
- 15:59Q&A: Inlining decisions
- 17:08Q&A: Library file timeouts
- 17:29Q&A: New IR validation
- 18:34Q&A: Incorrect optimizations
related talks
29mFlambda 2 Types: An abstract domain for static analysis of functional programs (mo...
22mEfficient OCaml compilation with Flambda 2
59mCompiler-assisted Translation Validation
15mInterleaving Large Language Models for Compiler Testing
01h 01mLive Lambda Calculus
01h 05mAll the Languages Together
23mBetter Defunctionalization through Lambda Set Specialization
15mFormulog: Datalog for SMT-Based Static Analysis