Towards Cumulative Abstract Semantics via Handlers
Cade Lueker, Andrew Fox, Bor-Yuh Evan Chang

TL;DR
This paper introduces a modular approach to abstract interpretation using scoped effects, enabling flexible, composable semantic analysis by separating syntax handling from semantic domain effects.
Contribution
It proposes a novel framework leveraging handlers for cumulative abstract semantics, enhancing modularity and flexibility in interpreters and static analyses.
Findings
Enables multiple evaluators from a single interpreter
Facilitates combining different path- and flow-sensitive analyses
Improves modularity and elegance of abstract interpretation implementations
Abstract
We consider the problem of modularizing control flow in a generic abstract interpretation framework. A generic abstract interpretation framework is not truly flexible if it does not allow interpreting with different path- and flow-sensitivities, by going forwards or backwards, and over- or under-approximately. Most interpreters inherently intertwine syntax and semantics, making the implementation antagonistic to modularity. Current approaches to modular designs require the use of complex data structures (e.g., monad transformers), providing modularity but often proving unwieldy (e.g., lifts). We observe that leveraging scoped effects within an interpreter facilitates the accumulation of semantic fragments against a fixed syntax. In this paper, we define cumulative abstract semantics, illustrating the potential for creating multiple dynamic evaluators and static analyses from one…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Logic, programming, and type systems · Formal Methods in Verification
