Stable relations and abstract interpretation of higher-order programs

on YouTube ↗31m

" summary

Defines a denotational semantics where terms are stable relations (binary relations between substitutions and values) and proves it sound and complete against the operational semantics; uses that collecting semantics with abstract interpretation to derive a modular relational analysis that infers input–output equalities and frame conditions for higher‑order code. Extends the correlations domain to support first‑class functions, implements the analyzer and formalizes proofs in Coq, gets precision on examples comparable to 1‑CFA, and notes loss of precision for unknown apply (returns top) and work remaining for exceptions.

AI-written summary · about

" chapters (17)

1. 0:00Stable relations intro
2. 1:06Frame conditions in analysis
3. 3:36Manual frames to abstract interpretation
4. 5:03Higher-order languages matter
5. 6:51Abstract interpretation for stable relations
6. 9:10Stability of input-output relations
7. 11:17Lambda terms as stable operations
8. 15:55Higher-order semantics
9. 18:28Modular static analysis from semantics
10. 21:43Precision and context sensitivity
11. 23:09Conclusions and future
12. 24:14Q&A: Preservation lemmas
13. 25:41Q&A: Operational vs functional
14. 26:22Q&A: Info loss in abstraction
15. 28:31Q&A: Flexibility of relations
16. 29:36Q&A: Proving functional correctness
17. 30:39Q&A: Static analysis without inputs