Retargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
summary
Claims that partially evaluating a sound abstract interpreter for S with a definitional interpreter for T yields a sound abstract interpreter for T, and mechanizes this with MetaOCaml. Demonstration uses an imperative S with fixed-size memory and a tiny single-register assembly T (add, mul); partial evaluation reuses S’s abstract operators and domain and produces joins and recursion mirroring the interpreter structure. Notable practical detail: using the second S memory cell as program counter makes T flow sensitivity depend on S’s sensitivity settings.
AI-written summary · about
related talks
18mCompiling with Abstract Interpretation
27mTaming Unsoundness with Gradual Abstract Interpretation
01h 01mA partial history of partial evaluation
30mAnalyzing Programs with SMT Solvers
23mTACAI: An Intermediate Representation based on Abstract Interpretation
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
20mCertified Abstract Machines for Skeletal Semantics