Towards Cumulative Abstract Semantics via Handlers (Short Paper)
summary
Proposes using algebraic effects to separate value creation and control flow: implement domain-specific introduction handlers (concrete ints, intervals with join) and syntax-eliminating elimination handlers (branching, non-branching, forward/backward sequencing) so one generic evaluator can be substantiated into concrete or abstract analyses by swapping handlers. Prototype on a tiny expression language and a Python subset shows handler swapping yields concrete evaluation, interval joins, and even backwards symbolic evaluation; implementation notes handling continuation-capture bugs (use a single effect type) and avoids monad-transformer lifting.
AI-written summary · about
chapters (8)
- 0:00Cumulative abstract semantics intro
- 0:42Simple expression language
- 2:06Abstract semantics components
- 3:29Control flow modulation
- 4:34Handlers introduction/elimination
- 7:02Combining handlers
- 8:26Demo and future work
- 8:50Q&A and related work
related talks
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
52mThink Abstractly, Work Concretely
22mToward Verified Library-Level Choreographic Programming with Algebraic Effects
33mExtensible Effects: A Leaner Cake for Purely Functional Code
20mOn Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
39mDesigning software with effects systems
36mThe Abstract Method, In General
25mComposing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming