Call-Guarded Abstract Definitional Interpreters
summary
A hybrid definitional interpreter called CGADI runs concrete semantics until a parameterized call guard forces abstraction, proving computability when the call-cache ordering is well-founded and monotone; two guards are implemented — a reentry guard that stays concrete on acyclic call paths and a size-change guard that detects descending arguments — and the prototype evaluates on a standard analysis corpus and a subset of LARC/R6RS, producing more precise results than a comparable CFA at low cost and often keeping execution fully concrete.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:27Overview of abstract interpreters
- 2:31Context sensitivity limits
- 7:25Goal of responsive analyzers
- 8:48Design of call-guarded interpreter
- 10:20Re-entry call guard
- 12:25Size change termination guard
- 17:06Ordering in size change
- 18:10Hybrid analysis evaluation
- 20:21Future work
- 21:19Q&A
related talks
20mAbstract Interpretation with Confidence
33mIntrinsically-Typed Definitional Interpreters à la Carte
27mTaming Unsoundness with Gradual Abstract Interpretation
25mFormalizing pi-Calculus in Guarded Cubical Agda
18mCompiling with Abstract Interpretation
24mThe Best of Abstract Interpretations
21mSynthesizing Formal Semantics from Executable Interpreters
20mCertified Abstract Machines for Skeletal Semantics
