Stable Relations and Abstract Interpretation of Higher-Order Programs
summary
Defines a denotational semantics for the untyped call-by-value lambda calculus as stable relations (monotone relations from substitutions to value sets) and proves it sound and complete against the small-step operational semantics, with an equivalent program logic. Uses that semantics as a collecting semantics, applies an independent-attribute-style abstraction plus an extended correlation domain for first-class functions, implements a bottom-up OCaml analyzer producing modular function summaries, and mechanically verifies proofs in Coq; prior first-order work proved 68% of invariants on an OS micro-kernel.
AI-written summary · about
chapters (9)
- 0:00Intro
- 1:03Static Analysis for Frame Inference Previous work
- 1:41Contributions
- 3:33The Property of Interest: Stable Relations
- 6:01A Denotation of Programs
- 7:40The Case of Variables
- 9:05Denotation for Functions
- 10:55Abstractions Steps
- 12:05A Modular Analysis
related talks
14mAdequacy for Algebraic Effects Revisited
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
24mTowards a Higher-Order Mathematical Operational Semantics
19mA Pure Demand Operational Semantics with Applications to Program Analysis
19mDeriving Dependently-Typed OOP from First Principles
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
49mSemantic Foundations for Probabilistic Programming
18mA Case for First-Class Environments