Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
summary
Introduces an abstract effect domain that summarizes context‑sensitive dependent effects as symbolic automata with accumulators, gives an abstract transformer for event prefixes, and embeds these abstractions in a cumulative type‑and‑effect system grounded in abstract interpretation. Implements an evDrift prototype for OCaml‑like code and runs 23 benchmarks, verifying 21 versus Drift 12, RCaml/Spacer 6, MoCHi 11, ReTHFL 18 and reporting multi‑fold speedups (6.3x, 5.3x, 16.8x, 6.4x). Targets history/register automata to express context‑free and input‑dependent temporal properties.
AI-written summary · about
chapters (7)
- 0:00Temporal safety verification intro
- 3:22Automated verification challenges
- 5:30Abstract interpretation for effects
- 9:04Type and effect system design
- 11:12Implementation and evaluation
- 12:36Summary and conclusion
- 13:19Q&A
related talks
14mTowards Cumulative Abstract Semantics via Handlers (Short Paper)
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
52mThink Abstractly, Work Concretely
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
27mTaming Unsoundness with Gradual Abstract Interpretation
22mHigher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
18mDeferring the Details and Deriving Programs
54mRevisiting the Evolution of Effects (Invited Talk)