Data Flow Refinement Type Inference

on YouTube ↗24m

" summary

DRIFT is a parametric abstract-interpretation framework that produces refinement-type systems and an inference algorithm; it implements numerical domains via the Apron library and supports octagon and polka (polyhedral) refinements plus configurable context sensitivity (call-stack length 1). The prototype runs on ~250 benchmarks, using widening (with/without thresholds) and 5-minute timeouts, and a context-sensitive loose-polka instantiation verifies 244 programs vs 217 for context-insensitive; overall it compares favorably to Dsolve and Mochi. APRON 244 verified programs

AI-written summary · about

" chapters (16)

1. 0:00Intro
2. 1:47Motivation (cont'd)
3. 3:29The Problem
4. 3:53Main Contribution
5. 5:12Concrete Semantics
6. 6:11Concrete Data Flow Semantics
7. 10:04Higher-order Functions
8. 13:02Concrete Data Flow Propagation
9. 13:52Concrete Transformer Example
10. 15:05Abstract Interpretation Framework
11. 17:12Collapsed Relational Data Flow Semantics
12. 18:01Parametric Refinement Data Flow Semantics
13. 18:43Parametric Type System
14. 19:42Liquid Type Semantics
15. 20:22Implementation & Evaluation
16. 23:02Summary